[Back]


Talks and Poster Presentations (with Proceedings-Entry):

D. Phan, J. Yang, M. Clark, R. Grosu, J. Schierman, S. Smolka, S. Stoller:
"A Component-Based Simplex Architecture for High-Assurance Cyber-Physical Systems";
Talk: Application of Concurrency to System Design (ACSD), 2017 17th International Conference on, Zaragoza, Spain; 2017-06-25 - 2017-06-30; in: "Application of Concurrency to System Design (ACSD), 2017 17th International Conference on", (2017), ISBN: 978-1-5386-2868-3; 49 - 58.



English 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.

Keywords:
collision avoidance;control engineering computing;large-scale systems;mobile robots;object-oriented programming;program verification;software architecture;theorem proving;A-G contracts;A-G proof rules;A-G reasoning;CBSA switching logic;assume-guarantee re


"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1109/ACSD.2017.23


Created from the Publication Database of the Vienna University of Technology.