Wednesday 28 Feb at 13:15 in EL41
Alexandre Donzé
Cyber-Physical Systems (CPS) are computerized systems interacting with their physical environments. They are prominent in transportation (car, plane, rockets), robotics, internet of things, etc. Control software for CPS has seen a dramatic increase in size and complexity in recent years. This is due to continuous pressure to optimize various aspects of the systems, such as, e.g., emissions and fuel efficiency in cars or more recently, the push toward more and more autonomous operations. The verification and validation of these software components are challenging because they are designed to influence and run in interaction with their physical environment. Ideally, testing necessitates a physical test-bed, a prototype, test tracks, etc. Such settings are costly and time-consuming, requiring hours in operating, collecting and analyzing data in order to get adequate confidence. An additional layer of complexity arises from the fact that control software components are increasingly reliant on machine learning (ML) components. Contrary to component based on so-called “traditional” control theory, ML-based components provide very little guarantees of accuracy, stability or performance.
Decyphir develops simulation-based and monitoring approaches, implemented in the tool Breach, that provide some pragmatic solutions to these challenges. The tool revolves first around a principle of separation of concerns: what is a typical test case and how do we generalize it? Can we use a formal language to specify whether a test succeeded or not and how far it was from failing/succeeding? If these two relatively simple questions are answered, the main ‘trick’ of Breach is to compose the resulting test-case generator and monitor with various optimization strategies to find rare cases of failure (falsification), improve coverage, etc. Breach has been used to find bugs in complex industrial-size models, and more recently we looked into the problem of testing CPS in interaction with ML-based components, such as computer vision systems based on deep neural net (DNN). Much has been done and said about how to fool a DNN, and we do not claim deep contributions there but rather want to make the case that such analysis should be performed at, or at least in consideration of system-level requirements. We illustrate this point this with a toy example instrumented by Breach involving a simple driving game simulator and an automatic emergency braking system (AEBS) using a custom Python-based neural net trained to detect red cows on the road.
Alexandre Donzé – Biography
Alexandre Donzé is CTO and co-founder of Decyphir, Inc, building design automation tools for Cyber-Physical Systems. In 2007, he graduated from Grenoble University with a Ph.D in Computer Science and Mathematics on simulation-based verification of hybrid systems. In 2007-2008, He was a post-doctoral faculty at Carnegie Mellon University, working with Edmund M. Clarke and Bruce H. Krogh, where he contributed to the popularization of Statistical Model Checking, a highly scalable formal verification technique. From 2009 to 2012 as a researcher at Verimag Lab in Grenoble, he contributed to the development of SpaceEx, a leading reachability analysis tool for hybrid systems while conducting original research on Systems Biology. In March 2012, he joined the Department of Electrical Engineering and Computer Science of the University of California at Berkeley. A major focus of his research has been the development and use of Signal Temporal Logic (STL), a formal specification language used for model-based design of Cyber-physical systems (CPS), circuits, biological systems, etc. He is the author of Breach, a Matlab toolbox supporting various simulation-based techniques using STL specifications, which is getting a wide adoption in both academia and industry. He co-founded Decyphir, Inc. in November 2016.
Alexandre Donzé is visiting SyTeC as a guest researcher during February 26 to March 2.
