Real-time reachability for verified simplex design

Stanley Bak, Taylor T. Johnson, Marco Caccamo, Lui Sha

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

46 Scopus citations


The Simplex Architecture ensures the safe use of an unverifiable complex controller by using a verified safety controller and verified switching logic. This architecture enables the safe use of high-performance, untrusted, and complex control algorithms without requiring them to be formally verified. Simplex incorporates a supervisory controller and safety controller that will take over control if the unverified logic misbehaves. The supervisory controller should (1) guarantee the system never enters and unsafe state (safety), but (2) use the complex controller as much as possible (minimize conservatism). The problem of precisely and correctly defining this switching logic has previously been considered either using a control-theoretic optimization approach, or through an offline hybrid systems reach ability computation. In this work, we prove that a combined online/offline approach, which uses aspects of the two earlier methods along with a real-time reach ability computation, also maintains safety, but with significantly less conservatism. We demonstrate the advantages of this unified approach on a saturated inverted pendulum system, where the usable region of attraction is 227% larger than the earlier approach.

Original languageEnglish
Title of host publicationProceedings - IEEE 35th Real-Time Systems Symposium, RTSS 2014
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages11
ISBN (Electronic)9781479972876
StatePublished - 14 Jan 2015
Externally publishedYes
Event35th IEEE Real-Time Systems Symposium, RTSS 2014 - Rome, Italy
Duration: 2 Dec 20145 Dec 2014

Publication series

NameProceedings - Real-Time Systems Symposium
ISSN (Print)1052-8725


Conference35th IEEE Real-Time Systems Symposium, RTSS 2014


  • hybrid systems
  • model checking
  • online
  • reachability computation
  • real-time reachability
  • verification


Dive into the research topics of 'Real-time reachability for verified simplex design'. Together they form a unique fingerprint.

Cite this