Formal Analysis for Stateflow Diagrams

Stateflow has been widely used in industry to specify and simulate control systems. Unfortunately, the lack of formal descriptions of Stateflow and its limited verification capability become an obstacle to handle complex systems working in safety-critical environment. In this paper, we apply a novel model checker named PAT to improve the reliability of Stateflow. We rigorously model the execution semantics of Stateflow in PAT´s expressive specification language. PAT´s simulation ability provides a means to validate our formal definitions of Stateflow. During the formalization procedure, we have discovered and corrected subtle flaws of Stateflow. Based on the PAT models of Stateflow, we can use PAT´s automatic reasoning power to verify complex systems against important requirements such as safety and liveness requirements.