Real-time reachability for verified simplex design

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

Research output: Contribution to journalArticlepeer-review


The Simplex architecture ensures the safe use of an unverifiable complex/smart controller by using it in conjunction with a verified safety controller and verified supervisory controller (switching logic). This architecture enables the safe use of smart, high-performance, untrusted, and complex control algorithms to enable autonomy without requiring the smart controllers to be formally verified or certified. Simplex incorporates a supervisory controller that will take over control from the unverified complex/smart controller if it misbehaves and use a safety controller. The supervisory controller should (1) guarantee that the system never enters an unsafe state (safety), but should also (2) use the complex/smart controller asmuch as possible (minimize conservatism). The problem of precisely and correctly defining the switching logic of the supervisory controller has previously been considered either using a control-theoretic optimization approach or through an offline hybrid-systems reachability computation. In this work, we show that a combined online/offline approach that uses aspects of the two earlier methods, along with a real-time reachability computation, also maintains safety, but with significantly less conservatism, allowing the complex controller to be used more frequently.We demonstrate the advantages of this unified approach on a saturated inverted pendulum system, inwhich the verifiable region of attraction is over twice as large compared to the earlier approach. Additionally, to validate the claims that the real-time reachability approach may be implemented on embedded platforms, we have ported and conducted embedded hardware studies using both ARM processors and Atmel AVR microcontrollers. This is the first ever demonstration of a hybrid-systems reachability computation in real time on actual embedded platforms, which required addressing significant technical challenges.

Original languageEnglish (US)
Article number2723871
JournalACM Transactions on Embedded Computing Systems
Issue number2
StatePublished - Feb 2016


  • Cyber-physical systems
  • Formal verification
  • Hybrid systems

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture


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

Cite this