Symbolic Simulation and Test Generation for Matlab Simulink/Stateflow
In model-based design methodology, a high-level model of a system is designed and subjected to analysis
before translating it to executable code.
is a popular commercial model-based
design tool for embedded control software. The common technique to analyze Simulink/Stateflow models is
to subject them to numerical simulations. This approach may not result in sufficient coverage of
the model due to various sources of non-determinism in the model, namely, initial states, inputs, and noise in the plant dynamics.
This work aims at improving the simulation coverage of Simulink/Stateflow models by
combining numerical simulations with symbolic techniques from verification.
A key contribution of our work is the formalization of the simulation semantics of Simulink/Stateflow models. Simulink updates the continuous state of a model by numerically integrating its derivatives at discrete-time steps. We therefore define the discrete-time concrete semantics of Simulink/Stateflow models. Figure (a) below shows a single step of concrete simulation.
The evaluation order between blocks of a Simulink/Stateflow model is determined by the MathWorks simulation engine.
We overcome the opacity in evaluation order semantics of Simulink/Stateflow by augmenting the concrete simultations
with symbolic simulations by instrumenting the model with callback functions. The instrumented code generates
the symbolic traces of simulations. Figure (b) shows the output of a single concrete plus symbolic simulation step. The output consists of a formula indicating the precondition on execution of the blocks
and the expression gives the symbolic expressions for the output variables of the block.
As the model is simulated numerically by Simulink, the symbolic trace is generated by our instrumentation code.
We use the idea of generating symbolic simulation trace generation to improve coverage of the model by generating test cases. Starting with a randomly-chosen initial state x (test input), we simulate the model both numerically
and symbolically. We then use the symbolic simulation trace and compute a set X of initial states that
are equivalent to x. This involves backward (possibly under-approximate)
preimage computation over the symbolic trace.
If the model is simulated with any state in X then the model is guaranteed
to follow the same discrete state transitions (under the same simulation parameters). Thus, the
set X can be declared to be covered and a new (non-redundant) initial state can be selected
from the complement of X. In our CAV 2009 paper, we have developed a new numerical domain,
called the bounded vertex representation,
for efficient under-approximate preimage computations of affine functions.
Software for instrumention and symbolic simulation
The ability to symbolically simulate Simulink/Stateflow models presents many possibilities for automated analysis. It is however challenging due to the complex semantics. Factors such as concurrency and hierarchy in Stateflow charts, triggered or conditional subsystems, and virtual blocks complicate the semantics.
In our existing implementation, listener functions are encoded for several types of blocks.
They monitor runtime values passing through the blocks and generate simulation traces.
You may need to extend similar functionality to other types of blocks.
The source code of our tool can be downloaded from here.
The directory src contains utility and high-level routines.
The routine add_listeners should be able to add listener blocks to your model and initialize data structures
maintained during the trace generation.
The framework is implemented for linear models only. The best way to get familiar with the implementation
and working of our tool is to try it on the Vehicle Climate Control demo model that comes with Simulink. Please note that we are no longer maintaining the implementation actively.
This tool is available under the Apache License, version 2.0.
Project completed: 2009