Real-time reachability for verified simplex design

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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 (US)
Title of host publicationProceedings - IEEE 35th Real-Time Systems Symposium, RTSS 2014
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages138-148
Number of pages11
EditionJanuary
ISBN (Electronic)9781479972876
DOIs
StatePublished - Jan 14 2015
Event35th IEEE Real-Time Systems Symposium, RTSS 2014 - Rome, Italy
Duration: Dec 2 2014Dec 5 2014

Publication series

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

Other

Other35th IEEE Real-Time Systems Symposium, RTSS 2014
CountryItaly
CityRome
Period12/2/1412/5/14

Keywords

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

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Computer Networks and Communications

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

  • Cite this

    Bak, S., Johnson, T. T., Caccamo, M., & Sha, L. (2015). Real-time reachability for verified simplex design. In Proceedings - IEEE 35th Real-Time Systems Symposium, RTSS 2014 (January ed., pp. 138-148). [7010482] (Proceedings - Real-Time Systems Symposium; Vol. 2015-January, No. January). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/RTSS.2014.21