Real-Time Reachability for Safety of Autonomous Systems
When: Monday, February 20, 2017
Where: PGH 563
Time: 10:00 – 11:00 AM
Speaker: Professor Taylor Johnson, Vanderbilt University
Host: Dr. Albert Cheng
The Simplex Architecture ensures the safe use of an unverifiable, complex controller such as those arising in autonomous systems by executing it in conjunction with a formally verified safety controller and a formally verified supervisory controller. Simplex enables the safe use of high-performance, untrusted, and complex control algorithms without requiring complex controllers to be formally verified or certified. The supervisory controller should take over control from an unverified complex controller if it misbehaves and transfer control to a safety controller. The supervisory controller should (1) guarantee the system never enters an unsafe state (safety), but should also (2) use the complex controller as much as possible (minimize conservatism). The problem of precisely and correctly defining the supervisory controller has previously been considered either using a control-theoretic optimization approach (LMIs), 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 in conjunction 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, where the verifiable region of attraction is over twice as large compared to the earlier approach. We present results of embedded hardware studies using both ARM processors on Beaglebone Black and Atmel AVR (Arduino) microcontrollers. This is the first ever demonstration of a hybrid systems reachability computation in real-time on actual embedded platforms, and required addressing significant technical challenges.
Taylor T. Johnson is an Assistant Professor of Electrical Engineering and Computer Science (EECS) at Vanderbilt University (since August 2016), where he directs the Verification and Validation for Intelligent and Trustworthy Autonomy Laboratory (VeriVITAL) and is a Senior Research Scientist in the Institute for Software Integrated Systems. Taylor was previously an Assistant Professor of Computer Science and Engineering (CSE) at the University of Texas at Arlington (September 2013 to August 2016). Taylor earned a PhD in Electrical and Computer Engineering (ECE) at the University of Illinois at Urbana-Champaign in 2013, an MSc in ECE at Illinois in 2010, and a BSEE in ECE from Rice University in 2008. Taylor's research focus is developing formal verification techniques and software tools for cyber-physical systems (CPS) with goals of improving safety, reliability, and security. Taylor has published over two-dozen papers on these verification and validation methods and their applications across domain areas such as power and energy systems, aerospace, transportation systems, and robotics, two of which were recognized with best paper awards, from the IEEE and IFIP, respectively. Taylor is a recipient of the AFOSR Young Investigator Program (YIP) award, and his research is supported by AFRL, AFOSR, NSF (CISE CCF/SHF, CNS/CPS; ENG ECCS/EPCN), NVIDIA, and USDOT.