Tools for Assurance-based Learning-enabled Cyber-Physical Systems: An Experience Report

ABSTRACT

Cyber-Physical Systems (CPS) are increasingly incorporating Learning-Enabled Components (LEC) to implement complex functions. By LEC we mean a component (typically, but not exclusively, realized in software) implemented with the help of data-driven techniques, e.g., machine learning. For example, an LEC in an autonomous car can implement a lane follower function such that one trains an appropriate convolutional neural network with a stream of images of the road as input and the observed actions of a human driver: steering, acceleration, breaking, etc., as output. The claim is that such LEC-s built via supervised learning are easier to implement than building a very complex, image processing driven control system that steers the car to follow the lane. In other words, if the straightforward design and engineering is too difficult, a neural network can do the job - after sufficient amount of training.

For high-consequence systems the challenge is to prove that the resulting system is safe: it does no harm, and it is live; i.e., it accomplishes its goals. Safety is perhaps the foremost problem in autonomous vehicles, especially for ones that operate in a less-regulated environment, like the open roads. The traditional technology for proving the safety of systems is based on extensively documented but often informal arguments - that are very hard to apply to CPS with LEC.

The talk will focus on experiences with a recent project that aims at changing this paradigm by introducing (1) verification techniques whenever possible (including proving properties of the 'learned' component), (2) monitoring technology for assurance to indicate when the LEC is not peforming well, and (3) formalizing the safety case argumentation process so that it can be dynamically evaluated. The application target is autonomous vehicles, that use LEC-s for selected functions. The goal was to construct an engineering process and a supporting toolchain that can be used for the systematic assurance of CPS with LEC-s.

Author

Dr. Gabor Karsai is Distinguished Professor of Computer Science and Electrical and Computer Engineering at Vanderbilt University and Senior Research Scientist at the Institute for Software-Integrated Systems. He has over thirty years of experience in research on systems and software engineering. He conducts research in the model-based design and implementation of cyber-physical systems, domain-specific languages, programming tools for visual programming environments, and the theory and practice of model-integrated computing. He received his BSc, MSc, and Dr. Techn. degrees from the Technical University of Budapest, in 1982, 1984 and 1988, respectively, and his PhD from Vanderbilt University in 1988. He has worked on several DARPA projects on advanced scheduling and resource management algorithms that resulted in a technology transitioned into all tactical aviation squadrons of the USMC, on fault-adaptive control technology that is used in aerospace applications, and on an information architecture platform for managed distributed real-time embedded software for fractionated spacecraft. Recently he has led an ARPA-E project on a Resilient Information Architecture Platform for Smart Grid that is currently used in a DOD project that is building a reusable, open-source microgrid control system. Since 2018 he is leading a DARPA project on the assurance-driven development of cyber-physical systems with learning-enabled software components.