slsf

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. Simulink/Stateflow 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.

Discrete-time concrete and symbolic simulation semantics

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.

See our CAV 2009 paper for complete discussion of our approach. In an earlier work (EMSOFT 2008), we mapped the concrete simulation trajectory to a manually constructed symbolic model.

Test generation and coverage of the initial state-space

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.

Publications

    • Rajeev Alur, Aditya Kanade, S. Ramesh, K.C. Shashidhar

    • Symbolic analysis for improving simulation coverage of Simulink/Stateflow models

    • Embedded Software (EMSOFT) 2008, ACM SIGBED EMSOFT best paper award

    • Aditya Kanade, Rajeev Alur, Franjo Ivančić, S. Ramesh, Sriram Sankaranarayanan, K.C. Shashidhar

    • Generating and analyzing symbolic traces of Simulink/Stateflow models

    • Computer Aided Verification (CAV) 2009

LICENSE

This tool is available under the Apache License, version 2.0.

Project completed: 2009