Symbolic verification of executable control specifications

Stateflow^TM is a MATLAB/Simulink toolbox that supports the development of executable specifications for discrete-state functions. It also supports general flowcharting of program functions. This paper describes a MATLAB program, sf2smv 2.0, that generates input for a symbolic model checking program, SMV, to verify properties of Stateflow^TM diagrams in Simulink. The SMV modules are constructed to reflect precisely the execution semantics in the simulation of Stateflow^TM diagrams. This extends previous work that created verification files that reflected an idealized version of the Stateflow^TM semantics. This paper describes how the principal Stateflow^TM execution rules are translated into SMV modules. Examples are used to illustrate the transformation procedures and their application to verify properties of executable specifications for control features in automotive powertrain control applications