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: |
| |||||||||
| ORCID: |
| |||||||||
| 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: |
| |||||||||
| 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
