Refinement-based verification of implementations of Stateflow charts

摘要

Simulink's Stateflow is a graphical notation widely adopted in industry. Since it is frequently used to model safety-critical systems, correctness of implementations of Stateflow charts is a major concern. In previous work, we have shown how we can generate formal models for refinement of Stateflow charts automatically. Here, we define a refinement strategy that supports the automated verification of implementations with respect to these models. We consider the verification of implementations that follow architectural patterns used in the Stateflow code generator. We present a detailed procedure for application of refinement laws. If the implementation is correct, the procedure succeeds. If a law application fails, the implementation is either incorrect or does not use the expected architectural pattern. The very low proof burden associated with the refinement verification makes a high level of automation possible.