Seminars

Advanced Analysis for Industrial Embedded Control Designs PDF
Jim Kapinski, Toyota

4/29/2014, 10:00pm, GHC 6501

Abstract

Model-based development (MBD) is a popular technique for performing embedded control system design for cyber-physical systems, such as automotive control systems. MBD designs are used to generate critical software, so it is vital to ensure correctness of these designs, but verification and validation (V&V) for MBD designs is a difficult and expensive process. This talk presents some perspective on the types of verification techniques currently available for MBD designs. We argue that new simulation-based techniques to increase confidence in system designs should be investigated, and we present one such technology that we are developing.

Our new analysis technique uses numerical simulations to perform Lyapunov analysis. Lyapunov functions for continuous dynamical systems are analogous to ranking functions for software systems; they can be used to certify convergence and also to obtain performance bounds on behaviors, but they are difficult to discover. Our technique uses simulation traces to discover candidate Lyapunov functions for nonlinear and hybrid dynamical systems. We iteratively improve the candidates using a search-based approach until we arrive at a sound result. We show how to certify the resulting analysis using either a satisfiability modulo theories (SMT) solver or a sampling-based approach. We present nonlinear and hybrid system examples, including an automotive powertrain control example.

Biography

Jim received his Ph.D. in Electrical and Computer Engineering from Carnegie Mellon University in 2005 and was a postdoctoral researcher at CMU from 2007 to 2008. He went on to found and lead Fixed-Point Consulting, serving clients in the defense, aerospace, and automotive industries. Since 2012 he has been with the Model-Based Development group at the Toyota Technical Center in Los Angeles, serving as a Principal Engineer. His work at Toyota focuses on advanced research into verification techniques for embedded software for powertrain control systems. Jim’s research interests involve verification techniques for embedded control system designs and analysis of hybrid dynamical systems.