CaltechAUTHORS
  A Caltech Library Service

Bisimulation conversion and verification procedure for goal-based control systems

Braman, Julia M. B. and Murray, Richard M. (2011) Bisimulation conversion and verification procedure for goal-based control systems. Formal Methods in System Design, 38 (1). pp. 62-95. ISSN 0925-9856 . https://resolver.caltech.edu/CaltechAUTHORS:20110308-123056956

Full text is not posted in this repository. Consult Related URLs below.

Use this Persistent URL to link to this item: https://resolver.caltech.edu/CaltechAUTHORS:20110308-123056956

Abstract

Fault tolerance and safety verification of control systems are essential for the success of autonomous robotic systems. A control architecture called Mission Data System (MDS), developed at the Jet Propulsion Laboratory, addresses these needs with a goal-based control approach. In this paper, a software algorithm for converting goal network control systems into linear hybrid systems is described. The conversion process is a bisimulation; the resulting linear hybrid system can be verified for safety in the presence of failures using existing symbolic model checkers, and thus the original goal network is verified. A moderately complex example goal network control system is converted to a linear hybrid system using the automatic conversion software that is based on the bisimulation and then is verified.


Item Type:Article
Related URLs:
URLURL TypeDescription
http://dx.doi.org/10.1007/s10703-010-0109-6 DOIUNSPECIFIED
http://www.springerlink.com/content/x6216nh672x24821/PublisherUNSPECIFIED
ORCID:
AuthorORCID
Murray, Richard M.0000-0002-5785-7481
Additional Information:© 2010 Springer Science, LLC. Published online: 22 December 2010. The authors would like to gratefully acknowledge Kenneth Meyer, Michel Ingham, David Wagner, Robert Rasmussen, Kirk Reinholtz, and the rest of the MDS team at JPL for feedback, suggestions, answered questions, and MDS and State Analysis instruction. This work was funded in part by the Air Force Office of Scientific Research (AFOSR) and The Boeing Company.
Funders:
Funding AgencyGrant Number
Air Force Office of Scientific Research (AFOSR)UNSPECIFIED
Boeing CompanyUNSPECIFIED
Subject Keywords:Verification; Hybrid systems; Model checking; Fault-tolerant control
Issue or Number:1
Record Number:CaltechAUTHORS:20110308-123056956
Persistent URL:https://resolver.caltech.edu/CaltechAUTHORS:20110308-123056956
Official Citation:Author: Braman, Julia Author: Murray, Richard Primary Title: Bisimulation conversion and verification procedure for goal-based control systems Journal Name: Formal Methods in System Design Cover Date: 2011-02-01 Publisher: Springer Netherlands Issn: 0925-9856 Subject: Computer Science Start Page: 62 End Page: 95 Volume: 38 Issue: 1 Url: http://dx.doi.org/10.1007/s10703-010-0109-6 Doi: 10.1007/s10703-010-0109-6
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:22716
Collection:CaltechAUTHORS
Deposited By: Ruth Sustaita
Deposited On:09 Mar 2011 17:16
Last Modified:03 Oct 2019 02:39

Repository Staff Only: item control page