As the automotive industry transitions towards model-based development, the need for model-based verification arises. Although recognized institutes such as ISO and IEC recognize the benefits of formal analysis in the development of safety-critical E/E systems, specific standards or guidelines on these practices are mostly absent. There are several toolsets available for formal verification purposes. These toolsets often use a niche modeling syntax which could hinder industry adaptation. By bridging the gap between widely used modeling software such as Simulink and verification tools we could enable the adoption of formal methods in the automotive or other safety-critical industries.
This work explored how formal verification can be applied to hierarchical Simulink and Simulink Stateflow models. By dividing the models into separate subsystems we can construct large hierarchical models in mCRL2 syntax, similar to the original hierarchy in Simulink. Several blocks in the Simulink block library have been translated to a functionally similar variant in mCRL2. Instances of these implementations can be placed in dataflow diagrams to obtain complex behaviour from a collection of simple processes. This process has been partially automated using a code generator which interprets mCRL2 design files as templates. This can reduce code repetition and makes the design process easier.
The approach has been demonstrated on a small toy example of the Collatz sequence, as well as a model from Mathworks’ examples repository, modeling a traffic intersection with two traffic lights. It could be demonstrated that the two variants of the Collatz model both converged to 1 for any of the given initial conditions.
The traffic light example model featured both dataflow blocks, virtual (subsystem) blocks and hierarchical Stateflow charts in which message queues are used to communicate between charts. Most effort in translating this model went into the Stateflow controller model, as this model used several Stateflow features (message queues and hierarchical charts) with limited documentation. As there is no formal definition of a dataflow or Stateflow diagram, the translation to mCRL2 has no formal basis. It can therefore not be demonstrated that the translation results in functionally equivalent models compared to the Simulink sources.
A SMT-based scheduling tool has been used to overcome the issue of incorrect schedules in dataflow diagrams due to an incorrect port ordering. This tool computes a satisfying schedule based on a simplified representation of the dataflow diagram. The resulting schedule can be imported in the template preprocessor to re-order the output ports.