Formal verification of implementations of Stateflow charts

Simulink diagrams are widely used in industry for specifying control systems, and a particular type of block used in them is a Stateflow chart. Often, the systems specified are safety-critical ones. Therefore, the issue of correctness of implementations of these systems is relevant. We are interested in the verification of implementations of Stateflow charts. In this thesis, we propose a formal model of Stateflow charts in the Circus notation. The proposed model makes a distinction between the general semantics of Stateflow charts and the specific aspects of each chart, and maintains the operational style used in the official informal description of the semantics of Stateflow. In this way, we support the comparison of our model to the informal description as an extra form of validation. Moreover, this separation allows us to obtain a translation from a Stateflow chart to a Circus model based mostly on the syntactic structure of the chart. We formalise in Z a translation strategy that supports the generation of the chart specific model which is composed with the model of the semantics of Stateflow charts to formalise the execution of the chart. The translation strategy is implemented in a tool that supports the automatic generation of the complete model of a chart. The style in which the translation strategy is specified supports a very direct implementation, thus, minimising this potential source of error. We identify an architecture of parallel implementations based on the sequential implementations automatically generated by a code generator, and propose a refinement strategy that applies the Circus refinement calculus to verify the correctness of the implementation with respect to the proposed formal model of Stateflow charts. The identification of the architecture allows us to specify the refinement strategy in a degree of detail that renders it suitable for formalisation in a tactical language, thus, potentially achieving a high degree of automation. Moreover, this strategy is a starting point for new strategies targeting different architectural patterns.