Refinement-based verification of sequential implementations of Stateflow charts

TL;DR

This paper presents a refinement-based verification method for automatically generated sequential C implementations of Stateflow charts, enhancing automation and supporting safety-critical control system verification.

Contribution

It introduces a refinement strategy tailored for verifying C implementations of Stateflow charts, leveraging architectural features for increased automation.

Findings

Supports formal verification of safety-critical control systems.

Enables higher automation in the verification process.

Applicable to sequential C implementations of Stateflow charts.

Abstract

Simulink/Stateflow charts are widely used in industry for the specification of control systems, which are often safety-critical. This suggests a need for a formal treatment of such models. In previous work, we have proposed a technique for automatic generation of formal models of Stateflow blocks to support refinement-based reasoning. In this article, we present a refinement strategy that supports the verification of automatically generated sequential C implementations of Stateflow charts. In particular, we discuss how this strategy can be specialised to take advantage of architectural features in order to allow a higher level of automation.