Will future cars have formally verified powertrain control software?Jyotirmoy V. Deshmukh, Toyota.
Abstract: Emerging technologies such as intelligent transportation systems, vehicles equipped with advanced driver assistance systems, self-driving vehicles, and vehicles with alternate energy sources have made the automotive industry an exciting field for a cyber-physical systems researcher. A fact often overlooked while developing these future technologies is that even a single automobile using a traditional powertrain is among the most complex cyber-physical systems designed by humans, and has design and verification challenges of considerable complexity. At the heart of an automobile are its engine and powertrain, whose operation is controlled by embedded software on an electronic control unit (ECU). The paradigm of model-based development (MBD) has become the de facto standard for designing such control software. MBD designs of control software range from feature-level models to application-level and even entire system-level models. On the other hand, models of the plant (e.g. the engine), can range from simple physics-based models to high-fidelity models. The advantage of MBD is in its ability to design, validate, and analyze the closed-loop model of the plant and the controller, often well before the actual hardware components become available. Unfortunately, even the simplest closed-loop model of an automotive powertrain subsystem is a complex cyber-physical system with highly nonlinear and hybrid dynamics, and reasoning about the correctness of such closed-loop models is a formidable task. To have formally verified powertrain control software in the future, several challenges would have to be surmounted. In this talk, we address two of these: What would be the formalisms used to express correctness and performance requirements for closed-loop models? What verification or bug-finding techniques would scale to existing and future engine control software? We survey some of the existing work done to address such questions, and present some promising directions for future work.
Biography: Jyotirmoy V. Deshmukh is a research engineer at Toyota Technical Center in Gardena (Los Angeles). His research interests are in the broad area of formal verification of cyberphysical systems, automatic synthesis and repair of systems, and temporal logic. His current focus is in the area of automotive control systems modeled as nonlinear and hybrid dynamical systems. Jyotirmoy got his Ph.D. in the area of verification for sequential and concurrent software at the University of Texas at Austin, and was a post-doctoral researcher mentored by Rajeev Alur at the University of Pennsylvania.