The ongoing renaissance in artificial intelligence (AI) has led to the advent of machine learning methods deployed within components for sensing, actuation, and control in safety-critical cyber-physical systems (CPS), and is enabling autonomy in such systems, such as autonomous vehicles, swarm robots, and other CPS with learning-enabled components. However, as demonstrated in part through recent accidents in semi-autonomous/autonomous CPS and by adversarial machine learning attacks, ensuring such components operate reliably in all scenarios is extraordinarily challenging. We will define and discuss specifying desired behaviors (e.g., for safety, security, robustness, and stability), using a real-time, real-valued temporal logic called hyperproperties for signal temporal logic that we have recently developed. We will discuss methods for assuring safety and security specifications in autonomous CPS using our nnv (neural network verification) tool, which has been applied to verify specifications for adaptive cruise control and autonomous emergency braking systems in motor vehicles. We will conclude with some architectural solutions that enhance trust and safety assurance in autonomous CPS, building on supervisory control with the Simplex architecture, and will discuss future research directions for enhancing trust of machine learning components within CPS that we are exploring within recently started DARPA Assured Autonomy and NSA/DoD Science of Security Lablet projects.
Dr. Taylor T. Johnson is an Assistant Professor of Computer Engineering, Computer Science, and Electrical Engineering in the Department of Electrical Engineering and Computer Science (EECS) at Vanderbilt University, 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. Dr. Johnson serves as the President of a medical information technology startup firm, CelerFama, Inc., and as the CTO of Verivital, LLC, both of which serve for technology transfer and commercialization of his research group's results to industry. Dr. Johnson was previously an Assistant Professor of Computer Science and Engineering at the UT Arlington (2013-16). Dr. Johnson earned a PhD in Electrical and Computer Engineering from UIUC in 2013, where he worked in CSL with Prof. Sayan Mitra. He has published over 70 papers on formal methods and their applications across cyber-physical systems (CPS) domains, such as power and energy, aerospace, automotive, transportation, biotechnology, and robotics, one of which was awarded an ACM Best Software Repeatability Award. Dr. Johnson is a 2018 and 2016 recipient of the AFOSR Young Investigator Program award, a 2015 recipient of the NSF CISE Research Initiation Initiative award, and his research is / has been supported by AFOSR, ARO, AFRL, DARPA, NSA, NSF, the MathWorks, NVIDIA, ONR, Toyota, and USDOT.