Paper Info
Title
Bisimulation conversion and verification procedure for goal-based control systems
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.
Year
DOI
Venue
2011
10.1007/s10703-010-0109-6
Formal Methods in System Design
Keywords
Field
DocType
Verification,Hybrid systems,Model checking,Fault-tolerant control
Model checking,Computer science,Real-time Control System,Jet propulsion,Real-time computing,Fault tolerance,Software,Bisimulation,Control system,Hybrid system,Distributed computing
Journal
Volume
Issue
ISSN
38
1
0925-9856
Citations 
PageRank 
References 
0
0.34
29
Authors
2
Name
Order
Citations
PageRank
Julia M. B. Braman120.73
Richard M. Murray2123221223.70