TY - JOUR
T1 - Real-time reachability for verified simplex design
AU - Johnson, Taylor T.
AU - Bak, Stanley
AU - Caccamo, Marco
AU - Sha, Lui
N1 - Funding Information:
The authors are grateful for the feedback from the anonymous reviewers of this article and its earlier revision [Bak et al. 2014] that significantly helped improve this article. The material presented in this article is based upon work supported by the National Science Foundation (NSF) under grant numbers CNS- 1302563, CNS-1219064, CNS 13-29886, CNS 13-30077, CNS 1464311, and CCF 1527398, by the Office of Naval Research (ONR) under grant number N00014-12-1-0046, by the Air Force Research Laboratory's Information Directorate (AFRL/RI) through the Visiting Faculty Research Program (VFRP) under contract number FA8750-13-2-0115, AFRL through contract number FA8750-15-1-0105, the Air Force Office of Scientific Research (AFOSR) in part under contract number FA9550-15-1-0258, and the AFOSR Summer Faculty Fellowship Program (SFFP). The U.S. government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the authors and do not necessarily reflect the views of the AFRL, AFRL/RI, AFOSR, NSF, or ONR.
Publisher Copyright:
© 2016 ACM.
PY - 2016/2
Y1 - 2016/2
N2 - 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.
AB - 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.
KW - Cyber-physical systems
KW - Formal verification
KW - Hybrid systems
UR - http://www.scopus.com/inward/record.url?scp=84964788955&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84964788955&partnerID=8YFLogxK
U2 - 10.1145/2723871
DO - 10.1145/2723871
M3 - Article
AN - SCOPUS:84964788955
SN - 1539-9087
VL - 15
JO - Transactions on Embedded Computing Systems
JF - Transactions on Embedded Computing Systems
IS - 2
M1 - 2723871
ER -