Proving properties of Stateflow models using ISO Standard Z and CADiZ

Abstract. This paper focuses on the use of ISO Standard Z and CADiZ in the formal validation of Stateflow models against requirements-oriented assumptions. It documents some of what the Simulink/Stateflow Analyser tool does in support of the Practical Formal Specification method. The tool aims to automate the formal validations of the method, so that users of Simulink/Stateflow can benefit from them. The Z exploits some notations that are particular to ISO Standard Z. The automation is aided by quite terse tactics interpreted by CADiZ.