Formal Verification of Simulink/Stateflow Diagrams

Simulink is an industrial de-facto standard for building executable models of control systems and their environments. Stateflow is a toolbox used to model reactive systems via hierarchical statecharts within a Simulink model, extending Simulink’s scope to event-driven and hybrid forms of embedded control. In safety-critical control systems, exhaustive coverage of system dynamics by formal verification would be desirable, being based on a formal semantics of combined Simulink/Stateflow graphical models. In our previous work, we addressed the problem of formal verification of pure Simulink diagrams via an encoding into HCSP, a formal modelling language encoding hybrid system dynamics by means of an extension of CSP. In this paper, we extend the approach to cover Simulink models containing Stateflow components also. The transformation from Simulink/Stateflow to HCSP is fully automatic, and the formal verification of the encoding is supported by a Hybrid Hoare Logic (HHL) prover based on Isabelle/HOL. We demonstrate our approach by a real world case study originating from the Chinese High-speed Train Control System (CTCS-3).