Name
Abstract | ||
|---|---|---|
We present Component-Based Simplex Architecture (CBSA), a new framework for assuring the runtime safety of component-based cyber-physical systems (CPSs). CBSA integrates Assume-Guarantee (A-G) reasoning with the core principles of the Simplex control architecture to allow component-based CPSs to run advanced, uncertified controllers while still providing runtime assurance that A-G contracts and global properties are satisfied. In CBSA, multiple Simplex instances, which can be composed in a nested, serial or parallel manner, coordinate to assure system-wide properties. Combining A-G reasoning and the Simplex architecture is a challenging problem that yields significant benefits. By utilizing A-G contracts, we are able to compositionally determine the switching logic for CBSAs, thereby alleviating the state explosion encountered by other approaches. Another benefit is that we can use A-G proof rules to decompose the proof of system-wide safety assurance into sub-proofs corresponding to the component-based structure of the system architecture. We also introduce the notion of coordinated switching between Simplex instances, a key component of our compositional approach to reasoning about CBSA switching logic. We illustrate our framework with a component-based control system for a ground rover. We formally prove that the CBSA for this system guarantees energy safety (the rover never runs out of power), and collision freedom (the rover never collides with a stationary obstacle). We also consider a CBSA for the rover that guarantees mission completion: all target destinations visited within a prescribed amount of time. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1109/ACSD.2017.23 | 2017 17th International Conference on Application of Concurrency to System Design (ACSD) |
Keywords | DocType | Volume |
Simplex architecture,Assume-guarantee reasoning,Component-based system architecture,Cyber-physical systems,Collision avoidance | Conference | abs/1704.04759 |
ISSN | ISBN | Citations |
1550-4808 | 978-1-5386-2868-3 | 1 |
PageRank | References | Authors |
0.37 | 15 | 7 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Dung Phan | 1 | 5 | 1.81 |
| Junxing Yang | 2 | 22 | 5.36 |
| Matthew Clark | 3 | 14 | 3.53 |
| Radu Grosu | 4 | 1011 | 97.48 |
| John D. Schierman | 5 | 1 | 0.37 |
| Scott A. Smolka | 6 | 2959 | 249.22 |
| Scott D. Stoller | 7 | 1320 | 89.10 |