Generating and Analyzing Symbolic Traces of Simulink/Stateflow ModelsAditya Kanade (University of Pennsylvania), Rajeev Alur (University of Pennsylvania), Franjo Ivancic (NEC Labs), S. Ramesh (GM India Science Lab)., Sriram Sankaranarayanan and K.C. Sashidhar (GM India Science Lab). |
|
We present a methodology and a toolkit for improving simulation
coverage of Simulink/Stateflow models of hybrid systems using
symbolic analysis of simulation traces. We propose a novel
instrumentation scheme that allows the simulation engine of
Simulink/Stateflow to output, along with the concrete simulation
trace, the symbolic transformers needed for our analysis.
Given a simulation trace, along with the symbolic transformers, our
analysis computes a set of initial states that would lead to
traces with the same sequence of discrete components at each step of
the simulation. Such an analysis relies critically on the use of
convex polyhedra to represent sets of states. However, the
exponential complexity of the polyhedral operations implies that the
performance of the analysis would degrade rapidly with the
increasing size of the model and the simulation traces. We propose a
new representation, called the \emph{bounded vertex representation}, which
allows us to perform under-approximate computations while fixing the
complexity of the representation \emph{a priori}. Using this
representation we achieve a trade-off between the complexity of the
symbolic computation and the quality of the under-approximation. We
demonstrate the benefits of our approach over existing simulation
and verification methods with case studies.
|
| ps pdf |
| Computer-aided Verification (CAV 2009), Volume ???? of Lecture Notes in Computer Science, pp. ???-???, Springer-Verlag. |
| Copyright (C) Springer-Verlag. Copy has been made available online for personal use only. Do not redistribute without permission. |