EMBEDDED SYSTEMS WEEK

Tutorial T4

Title: Neural Network and Autonomous Cyber-Physical Systems Formal Verification for Trustworthy AI and Safe Autonomy

Abstract:

This interactive tutorial will describe state-of-the-art methods for formally verifying neural networks and their usage within safety-critical cyberphysical systems (CPS). The tutorial will begin with a lecture on this emerging research area, followed by demos of these methods implemented in software tools, specifically the Neural Network Verification (NNV) tool. Examples will include systems from aerospace, automotive, and beyond. In this tutorial, we will demonstrate NNV capabilities through a collection of safety and robustness verification tasks, which involve the reachable set computation of feedforward, convolutional, semantic segmentation, and recurrent neural networks, as well as neural ordinary differential equations and neural network control systems. The tutorial will be interactive, and as NNV is publicly available, participants can follow along as desired. Publications on NNV have participated in several prior repeatability/artifact evaluations at top conferences such as CAV, with passing results for multiple publications, which illustrates the feasibility of this interactive demonstration plan. Further. NNV is already available for in-browser execution through platforms like CodeOcean, and we plan to organize the interactive tutorial aspects around this or similar (Jupyter-like) in-browser demonstrations.

Presenters

Hoang-Dung Tran, Ph.D. is an Assistant Professor in the School of Computing at the University of Nebraska, Lincoln. He is a co-director of the NIMBUS Lab at UNL, where he leads the Verification and Validation for Assured Autonomy group (V2A2). He earned a Ph.D. degree in Computer Science at Vanderbilt University in August 2020. His research interests are specification language, formal verification, monitoring, safe control, planning, and learning for autonomous cyber-physical systems (CPS), focusing on in-road and off-road autonomous driving, human-robot interaction in construction, and surgery. His group develops both software and hardware prototypes for their research. Dr. Tran has been developing the NNV (Neural Network Verification) framework for Deep Neural Networks and Learning-enabled CPS. The NNV tool is used in Northrop Grumman for the DARPA Assured Autonomy project and is partially supported by Toyota Research. His work on verification of learning-enabled CPS has won the prestigious IEEE TCCPS outstanding dissertation award 2021.

Diego Manzanas Lopez, PhD is a Computer Science (CS) Postdoctoral Scholar at the Institute for Software Integrated Systems at Vanderbilt University, where he received his Ph.D. degree in electrical engineering in 2022. His main research interests lie in the intersection of Cyber-Physical Systems (CPS), deep learning (DL) and formal methods. During his research career, he has published over 25 papers in the areas of formal verification for autonomous systems with learning enable components (LECs), and the formal verification of deep learning models such Convolutional Neural Networks and Neural Ordinary Differential Equations, in venues such as CAV, EMSOFT, FM, FORMATS, and JAT. He has also contributed to the development of the open-source Neural Network Verification (NNV) software tool to implement these techniques and formally verify case studies in multiple domains including semantic segmentation, image classification, and control systems for safety-critical applications. He also enjoys working with autonomous vehicles, as he has been a member of the Vanderbilt team during his PhD in two F1/10 competitions (2019 CPS-IoT Week and 2019 Embedded Systems week) and at the 2019 NSF CPS Challenge.

Taylor T. Johnson, PhD, PE is A. James and Alice B. Clark Foundation Chancellor Faculty Fellow and Associate Professor of Computer Science (CS) 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 (ISIS). Dr. Johnson’s research focus is developing formal verification techniques and software tools for cyber-physical systems (CPS), with a focus most recently on autonomous CPS that incorporate artificial intelligence (AI) and machine learning (ML) components, such as neural networks, for tasks ranging from sensing/ perception through planning/control. Dr. Johnson has published around a hundred papers on these methods and their applications across CPS domains, such as power and energy systems, aerospace and avionics systems, automotive systems, transportation systems, and robotics in venues such as CAV, EMSOFT, FM, ICCPS, ICDM, ICSE, MEMOCODE, NFM, RTSS, TNNLS, and UAI. Dr. Johnson received the AFOSR Summer Faculty Fellowship Program (SFFP) award to visit the Air Force Research Laboratory (AFRL)’s Information Directorate in 2015, was a Visiting Faculty Research Program (VFRP) award fellow at AFRL’s Information Directorate in 2014, and was a visiting graduate research assistant through an SFFP award at AFRL’s Space Vehicles Directorate at Kirtland Air Force Base in 2011. Taylor is a 2018 and 2016 recipient of the AFOSR Young Investigator Program (YIP) award, a 2015 recipient of the NSF Computer and Information Science and Engineering (CISE) Research Initiation Initiative (CRII), and his research is / has been supported by AFRL, AFOSR, ARO, DARPA, Mathworks, NSA, NSF (CISE CCF/SHF, 4 CCF/FMitF, CNS/CPS; ENG ECCS/EPCN), NVIDIA, ONR, Toyota, and USDOT.