Aerospace Department Seminar | Automated Formal Verification for Aerospace Cyber-Physical Systems
Automated Formal Verification for Aerospace Cyber-Physical Systems
Taylor T. Johnson
Computer Science and Engineering
University of Texas at Arlington
Defects in cyber-physical systems (CPS) are prevalent as exemplified by certain FAA Airworthiness Directives (ADs) in aerospace systems, as well as recalls of motor vehicles by the NHTSA and medical devices by the FDA. Defects in CPS may stem from the interaction of cyber (software) and physical systems, and we illustrate this through pertinent aerospace systems, such as Ariane 5 flight 501 and recent FAA ADs. To address this growing challenge for these increasingly complex safety-critical systems, our research vision is to develop novel formal methods to verify automatically that CPS satisfy their specifications, where we typically model CPS as hybrid systems that have mixed continuous and discrete dynamics. This talk focuses on our verification of safe separation between aircraft in a distributed air traffic control protocol for general aviation from NASA LaRC that arose as a candidate component of the FAA's NextGen air transportation system. In this protocol, we model each aircraft as a communicating hybrid system in a parameterized network. Our approach is implemented in our Passel software tool, and enabled the automatic verification of safety for this protocol regardless of the number of aircraft involved. We conclude with an overview of some of our ongoing research projects in CPS verification, such as: a novel Simplex architecture that uses our real-time reachability algorithm for hybrid systems (now being prototyped for avionics with NASA LaRC), collision-free distributed formation control algorithms for Unmanned Aircraft Systems (UAS), and correct-by-construction controller implementation in Simulink/Stateflow using our HyST software tool.
About the speaker...
Taylor T. Johnson is an Assistant Professor of Computer Science and Engineering at the University of Texas at Arlington, where he directs VeriVITAL (the Verification and Validation for Intelligent and Trustworthy Autonomy Laboratory). Dr. Johnson 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. Dr. Johnson's research focus is to develop formal verification techniques and software tools for cyber-physical systems (CPS) with goals of improving CPS safety, reliability, and security, while applying and advancing foundational results from hybrid systems, formal methods, control theory, distributed systems, and real-time systems. Dr. Johnson has published over thirty papers on these formal methods and their applications across domains including aerospace systems, power and energy systems, and robotics, two of which were recognized with best paper awards, from the IEEE and IFIP, respectively. Dr. Johnson's research is supported by AFRL, AFOSR, NSF (CISE CCF/SHF, CISE CNS/CPS, ENG ECCS/EPCN), NVIDIA, and USDOT. Dr. Johnson is a member of ACM, AIAA, IEEE, and SAE.