Title: Symbolic Analysis of Simulations of Embedded System Designs
Speaker: Aditya Kanade
Affiliation: Univ. of Pennsylvania (Postdoctoral Research Associate)
Date: February 5, 2009
Abstract:
Embedded control software is used for controlling physical systems, like elevators, cars, and aircrafts, operating in safety-critical situations. Embedded system models can be subjected to simulation-based analysis. While this technique is applicable to complex systems, it cannot give formal guarantees about correctness of models. The prohibitive complexity of symbolic computations over numerical domains, on the other hand, limits the verification techniques to systems with a small number of continuous variables.
In this work, we have developed a technique that improves effectiveness of simulations by combining numerical simulations with symbolic methods for computing state-sets. Given a simulation trace, our algorithm computes a set of states that are equivalent to the initial state of the simulation trace. Thus with a single simulation, we can declare a non-trivial region of the initial state-space as covered. We have developed new techniques based on the scalable computational method of linear programming to compute and manipulate symbolic representations of convex polyhedra.
Our analysis tool is completely automated and works on models developed with the industrial tool MATLAB Simulink/Stateflow. We have evaluated our tool on Simulink demos from Mathworks, hybrid systems verification benchmarks and real-world case studies from General Motors.
(Joint work with Rajeev Alur, Franjo Ivancic, S. Ramesh, Sriram Sankaranarayanan and K.C. Shashidhar)