Verification of Discrete and Hybrid Powertrain Controllers

Bruce H. Krogh Professor, Carnegie Mellon University Verification of embedded control features for automotive powertrains early in the development process offers an enormous potential for reducing the time and cost to realize production control systems. An effective verification tool must work directly on models already being developed for simulation and automatic code generation. Recently, we have developed two tools at Carnegie Mellon University that use the Simulink/Stateflow user interface as the front-end for symbolic verification of discrete and hybrid dynamic systems. One tool is a Matlab command, sf2smv, which generates input files for the finite-state model checker SMV directly from Stateflow charts. The other tool generates finite-state approximations to hybrid system dynamics represented in a Simulink/Stateflow block diagram. Logical assertions for the hybrid system behavior can then be verified. The finite-state approximations are refined automatically when the verification result is inconclusive. In this presentation, these two tools will be demonstrated for representative examples of embedded powertrain controllers. The theory behind the tools will be reviewed briefly. Directions for further development and their application to automotive control problems will also be discussed.