Rice University

Events at Rice

Seminar

Electrical and Computer Engineering
Dean of Engineering
Faculty Host: Lin Zhong

Speaker: Taylor Johnson '08
Assistant Professor, EECS
Vanderbilt University

ECE Semina Series: Real-Time Reachability for Verification of Autonomous Cyber-Physical Systems (698/699)

Friday, March 3, 2017
4:00 PM  to 5:00 PM

101  Keck Hall
Rice University
6100 Main St
Houston, Texas, USA

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. We will conclude with ongoing research on formally modeling and verifying CPS, including swarm robotics controlled with distributed algorithms, automotive CPS, aerospace CPS include groups of UAVs, and developing fundamental new modeling abstractions for designing CPS using extensions of Signal Temporal Logic (STL) done in conjunction with Toyota.

Biography of Taylor Johnson '08:
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 is a 2016 recepient of the AFOSR Young Investigator Research Program (YIP) award. 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 three-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, and one of which was recognize with a Best Software Repeatability award from the ACM. Taylor gratefully acknowledges the support of his group's research by AFRL, AFOSR, ARO, NSF (CISE CCF/SHF, CNS/CPS; ENG ECCS/EPCN), NVIDIA, ONR, Toyota, and USDOT.



<<   March 2017   >>
S M T W T F S
1 2 3 4
5 6 7 8 9 10 11
12 13 14 15 16 17 18
19 20 21 22 23 24 25
26 27 28 29 30 31

Search for Events


Quicklinks