{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,28]],"date-time":"2026-03-28T20:31:39Z","timestamp":1774729899585,"version":"3.50.1"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2016,2,17]],"date-time":"2016-02-17T00:00:00Z","timestamp":1455667200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2016,6,7]]},"abstract":"<jats:p>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 as much 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, in which 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.<\/jats:p>","DOI":"10.1145\/2723871","type":"journal-article","created":{"date-parts":[[2016,2,22]],"date-time":"2016-02-22T13:07:16Z","timestamp":1456146436000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":35,"title":["Real-Time Reachability for Verified Simplex Design"],"prefix":"10.1145","volume":"15","author":[{"given":"Taylor T.","family":"Johnson","sequence":"first","affiliation":[{"name":"University of Texas at Arlington, Arlington, TX"}]},{"given":"Stanley","family":"Bak","sequence":"additional","affiliation":[{"name":"Air Force Research Laboratory, Wright-Patterson AFB, OH"}]},{"given":"Marco","family":"Caccamo","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign"}]},{"given":"Lui","family":"Sha","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign"}]}],"member":"320","published-online":{"date-parts":[[2016,2,17]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.2514\/6.2010-8041"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_4_1","volume-title":"Viability Theory","author":"Aubin Jean-Pierre","unstructured":"Jean-Pierre Aubin . 1991. Viability Theory . Birkhauser Boston Inc ., Cambridge, MA. Jean-Pierre Aubin. 1991. Viability Theory. Birkhauser Boston Inc., Cambridge, MA."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_2_1_6_1","volume-title":"Industrial Application of the System-Level Simplex Architecture for Real-Time Embedded System Safety. Master\u2019s thesis","author":"Bak Stanley","unstructured":"Stanley Bak . 2009. Industrial Application of the System-Level Simplex Architecture for Real-Time Embedded System Safety. Master\u2019s thesis . University of Illinois at Urbana-Champaign , Champaign, IL . Stanley Bak. 2009. Industrial Application of the System-Level Simplex Architecture for Real-Time Embedded System Safety. Master\u2019s thesis. University of Illinois at Urbana-Champaign, Champaign, IL."},{"key":"e_1_2_1_7_1","volume-title":"Retrieved","author":"Bak Stanley","year":"2013","unstructured":"Stanley Bak . 2013 a. HyCreate: A Tool for Overapproximating Reachability of Hybrid Automata . Retrieved January 17, 2016 from http:\/\/stanleybak.com\/projects\/hycreate\/hycreate.html. Stanley Bak. 2013a. HyCreate: A Tool for Overapproximating Reachability of Hybrid Automata. Retrieved January 17, 2016 from http:\/\/stanleybak.com\/projects\/hycreate\/hycreate.html."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2728606.2728630"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2009.20"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2010.27"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2014.21"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS.2011.25"},{"key":"e_1_2_1_14_1","volume-title":"UPPAAL: A tool suite for automatic verification of real-time systems","author":"Bengtsson Johan","year":"1996","unstructured":"Johan Bengtsson , Kim Larsen , Fredrik Larsson , Paul Pettersson , and Wang Yi . 1996 . UPPAAL: A tool suite for automatic verification of real-time systems . In Hybrid Systems III, Rajeev Alur, Thomas Henzinger, and Eduardo Sontag (Eds.). Lecture Notes in Computer Science, Vol. 1066 . Springer , Berlin, 232--243. DOI:http:\/\/dx.doi.org\/10.1007\/BFb0020949 10.1007\/BFb0020949 Johan Bengtsson, Kim Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. 1996. UPPAAL: A tool suite for automatic verification of real-time systems. In Hybrid Systems III, Rajeev Alur, Thomas Henzinger, and Eduardo Sontag (Eds.). Lecture Notes in Computer Science, Vol. 1066. Springer, Berlin, 232--243. DOI:http:\/\/dx.doi.org\/10.1007\/BFb0020949"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1002\/rnc.2914"},{"key":"e_1_2_1_16_1","volume-title":"Linear Matrix Inequalities in System and Control Theory. Studies in Applied Mathematics","volume":"15","author":"Boyd S.","unstructured":"S. Boyd , L. El Ghaoui , E. Feron , and V. Balakrishnan . 1994 . Linear Matrix Inequalities in System and Control Theory. Studies in Applied Mathematics , Vol. 15 . SIAM, Philadelphia, PA. S. Boyd, L. El Ghaoui, E. Feron, and V. Balakrishnan. 1994. Linear Matrix Inequalities in System and Control Theory. Studies in Applied Mathematics, Vol. 15. SIAM, Philadelphia, PA."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/9.664150"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2000367.2000368"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2012.70"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1338441.1338673"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/646878.710295"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1755952.1755956"},{"key":"e_1_2_1_25_1","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, Christel Baier and Cesare Tinelli (Eds.)","author":"Duggirala Parasara Sridhar","unstructured":"Parasara Sridhar Duggirala , Sayan Mitra , Mahesh Viswanathan , and Matthew Potok . 2015. C2E2: A verification tool for stateflow models . In Tools and Algorithms for the Construction and Analysis of Systems, Christel Baier and Cesare Tinelli (Eds.) . Lecture Notes in Computer Science , Vol. 9035 . Springer , Berlin , 68--82. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-662-46681-0_5 10.1007\/978-3-662-46681-0_5 Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan, and Matthew Potok. 2015. C2E2: A verification tool for stateflow models. In Tools and Algorithms for the Construction and Analysis of Systems, Christel Baier and Cesare Tinelli (Eds.). Lecture Notes in Computer Science, Vol. 9035. Springer, Berlin, 68--82. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-662-46681-0_5"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/2555754.2555780"},{"key":"e_1_2_1_27_1","series-title":"Lecture Notes in Computer Science","volume-title":"Improving SAT modulo ODE for hybrid systems analysis by combining different enclosure methods","author":"Eggers Andreas","unstructured":"Andreas Eggers , Nacim Ramdani , Nedialko Nedialkov , and Martin Fr\u00e4nzle . 2011. Improving SAT modulo ODE for hybrid systems analysis by combining different enclosure methods . In Software Engineering and Formal Methods, Gilles Barthe, Alberto Pardo, and Gerardo Schneider (Eds.). Lecture Notes in Computer Science , Vol. 7041 . Springer Berlin , 172--187. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-642-24690-6_13 10.1007\/978-3-642-24690-6_13 Andreas Eggers, Nacim Ramdani, Nedialko Nedialkov, and Martin Fr\u00e4nzle. 2011. Improving SAT modulo ODE for hybrid systems analysis by combining different enclosure methods. In Software Engineering and Formal Methods, Gilles Barthe, Alberto Pardo, and Gerardo Schneider (Eds.). Lecture Notes in Computer Science, Vol. 7041. Springer Berlin, 172--187. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-642-24690-6_13"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0062-x"},{"key":"e_1_2_1_29_1","volume-title":"Alexandre Donz\u00e9, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler.","author":"Frehse Goran","year":"2011","unstructured":"Goran Frehse , Colas Le Guernic , Alexandre Donz\u00e9, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011 . SpaceEx: Scalable verification of hybrid systems. In Computer Aided Verification (CAV). Lecture Notes in Computer Science. Springer , Berlin. Goran Frehse, Colas Le Guernic, Alexandre Donz\u00e9, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011. SpaceEx: Scalable verification of hybrid systems. In Computer Aided Verification (CAV). Lecture Notes in Computer Science. Springer, Berlin."},{"key":"e_1_2_1_30_1","volume-title":"International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201913)","author":"Gao Sicun","year":"2013","unstructured":"Sicun Gao , Soonho Kong , and Edmund Clarke . 2013 . Satisfiability modulo ODEs . In International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201913) . DOI:http:\/\/dx.doi.org\/10.1109\/FMCAD.2008.ECP.14 10.1109\/FMCAD.2008.ECP.14 Sicun Gao, Soonho Kong, and Edmund Clarke. 2013. Satisfiability modulo ODEs. In International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201913). DOI:http:\/\/dx.doi.org\/10.1109\/FMCAD.2008.ECP.14"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562117"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.arcontrol.2009.03.002"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050008"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/225058.225162"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1089014.1089020"},{"key":"e_1_2_1_36_1","volume-title":"Johnson and Sayan Mitra","author":"Taylor","year":"2014","unstructured":"Taylor T. Johnson and Sayan Mitra . 2014 . Anonymized reachability of rectangular hybrid automata networks. In Formal Modeling and Analysis of Timed Systems (FORMATS\u2019 14). Taylor T. Johnson and Sayan Mitra. 2014. Anonymized reachability of rectangular hybrid automata networks. In Formal Modeling and Analysis of Timed Systems (FORMATS\u201914)."},{"key":"e_1_2_1_37_1","volume-title":"IEEE Conference on Computer-Aided Control System Design. 98--103","author":"Kapinski J.","unstructured":"J. Kapinski and B. H. Krogh . 2002. A new tool for verifying computer controlled systems . In IEEE Conference on Computer-Aided Control System Design. 98--103 . J. Kapinski and B. H. Krogh. 2002. A new tool for verifying computer controlled systems. In IEEE Conference on Computer-Aided Control System Design. 98--103."},{"key":"e_1_2_1_38_1","volume-title":"Nonlinear Systems","author":"Khalil H. K.","unstructured":"H. K. Khalil . 2002. Nonlinear Systems ( 3 rd ed.). Prentice Hall , Upper Saddle River, NJ. H. K. Khalil. 2002. Nonlinear Systems (3rd ed.). Prentice Hall, Upper Saddle River, NJ.","edition":"3"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/PL00009858"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS.2012.10"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2013.50"},{"key":"e_1_2_1_42_1","volume-title":"-S. Liu","author":"Lin Kwei-Jay","year":"1987","unstructured":"Kwei-Jay Lin , Swaminathan Natarajan , and Jane W . -S. Liu . 1987 . Imprecise results: Utilizing partial computations in real-time systems. In RTSS. 210--217. Kwei-Jay Lin, Swaminathan Natarajan, and Jane W.-S. Liu. 1987. Imprecise results: Utilizing partial computations in real-time systems. In RTSS. 210--217."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/321738.321743"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.259428"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/CACSD.2004.1393890"},{"key":"e_1_2_1_46_1","series-title":"Lecture Notes in Computer Science","volume-title":"ModelPlex: Verified runtime validation of verified cyber-physical system models","author":"Mitsch Stefan","unstructured":"Stefan Mitsch and Andre Platzer . 2014. ModelPlex: Verified runtime validation of verified cyber-physical system models . In Runtime Verification, Borzoo Bonakdarpour and Scott A. Smolka (Eds.). Lecture Notes in Computer Science , Vol. 8734 . Springer , Berlin , 199--214. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-319-11164-3_17 10.1007\/978-3-319-11164-3_17 Stefan Mitsch and Andre Platzer. 2014. ModelPlex: Verified runtime validation of verified cyber-physical system models. In Runtime Verification, Borzoo Bonakdarpour and Scott A. Smolka (Eds.). Lecture Notes in Computer Science, Vol. 8734. Springer, Berlin, 199--214. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-319-11164-3_17"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2461446.2461456"},{"key":"e_1_2_1_48_1","volume-title":"Interval Analysis","author":"Moore R. E.","unstructured":"R. E. Moore . 1966. Interval Analysis . Prentice-Hall . R. E. Moore. 1966. Interval Analysis. Prentice-Hall."},{"key":"e_1_2_1_49_1","volume-title":"Simplex Architecture for Run Time Assurance of Hybrid Systems. Safe and Secure Systems and Software Symposium (S5).","author":"Murthy Abhishek","year":"2012","unstructured":"Abhishek Murthy . 2012 . Simplex Architecture for Run Time Assurance of Hybrid Systems. Safe and Secure Systems and Software Symposium (S5). Abhishek Murthy. 2012. Simplex Architecture for Run Time Assurance of Hybrid Systems. Safe and Secure Systems and Software Symposium (S5)."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(94)00008-O"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1137\/050638448"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1210268.1210276"},{"key":"e_1_2_1_53_1","volume-title":"Marz","author":"Seto Danbing","year":"2000","unstructured":"Danbing Seto , Enrique Ferreira , and Theodore F . Marz . 2000 . Case Study : Development of a Baseline Controller for Automatic Landing of an F-16 Aircraft using Linear Matrix Inequalities (LMIs). Carnegie Mellon University Software Engineering Institute , Pittsburgh, PA 15213. Technical report number CMU\/SEI-99-TR-020. http:\/\/www.sei.cmu.edu\/reports\/99tr020.pdf. Danbing Seto, Enrique Ferreira, and Theodore F. Marz. 2000. Case Study: Development of a Baseline Controller for Automatic Landing of an F-16 Aircraft using Linear Matrix Inequalities (LMIs). Carnegie Mellon University Software Engineering Institute, Pittsburgh, PA 15213. Technical report number CMU\/SEI-99-TR-020. http:\/\/www.sei.cmu.edu\/reports\/99tr020.pdf."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2001.936213"},{"key":"e_1_2_1_56_1","unstructured":"T. S\u00f6derstr\u00f6m and P. Stoica (Eds.). 1988. System Identification. Prentice-Hall Inc. Upper Saddle River NJ.  T. S\u00f6derstr\u00f6m and P. Stoica (Eds.). 1988. System Identification. Prentice-Hall Inc. Upper Saddle River NJ."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-007-0044-3"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1080\/10556789908805762"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0895479896303430"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2502524.2502531"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2012.2219060"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2723871","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2723871","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:16:43Z","timestamp":1750227403000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2723871"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,2,17]]},"references-count":57,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,6,7]]}},"alternative-id":["10.1145\/2723871"],"URL":"https:\/\/doi.org\/10.1145\/2723871","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,2,17]]},"assertion":[{"value":"2014-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-02-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}