Proving Properties of Stateflow Models Using ISO Standard Z and CADiZ

  • Ian Toyn
  • Andy Galloway
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3455)


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.


Model Check Inference Rule Decision Procedure Source State Healthiness Condition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Toyn, I., McDermid, J.: CADiZ: An architecture for Z tools and its implementation. Software — Practice and Experience 25, 305–330 (1995)CrossRefGoogle Scholar
  2. 2.
    Toyn, I.: CADiZ on-line documentation (2005),
  3. 3.
    ISO/IEC: Information Technology—Z Formal Specification Notation—Syntax, Type System and Semantics , International Standard 13568:2002 (2002),
  4. 4.
    The MathWorks: Matlab and Simulink for technical computing (2005),
  5. 5.
    Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8, 231–274 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Arthan, R., Caseley, P., O’Halloran, C., Smith, A.: ClawZ: Control laws in Z. In: ICFEM 2000: 3rd IEEE International Conference on Formal Engineering Methods, pp. 169–176 (2000)Google Scholar
  7. 7.
    Toyn, I.: Simulink/Stateflow Analyser user’s manual. Technical report, Dept of Computer Science, University of York (2005)Google Scholar
  8. 8.
    Galloway, A., Cockram, T., McDermid, J.: Experiences with the application of discrete formal methods to the development of engine control software. In: Proceedings of Distributed Computer Control Systems (DCCS), IFAC (1998)Google Scholar
  9. 9.
    McDermid, J., Galloway, A., Burton, S., Clark, J., Toyn, I., Tracey, N., Valentine, S.: Towards industrially applicable formal methods: Three small steps, and one giant leap. In: International Conference on Formal Engineering Methods, pp. 76–88. IEEE Press, Los Alamitos (1998)Google Scholar
  10. 10.
    Iwu, F., Galloway, A., Toyn, I., McDermid, J.: Practical Formal Specification for embedded control systems. In: INCOM 2004: 11th IFAC Symposium on Information Control Problems in Manufacturing (2004)Google Scholar
  11. 11.
    Blow, J., Galloway, A.: Generalised substitution language and differentials. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 396–415. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. 12.
    Toyn, I.: Innovations in the notation of Standard Z. In: P. Bowen, J., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol. 1493, pp. 193–214. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  13. 13.
    Shostak, R.: On the SUP-INF method for proving Presburger formulas. JACM 24, 529–543 (1977)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new Symbolic Model Verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  15. 15.
    Toyn, I.: A tactic language for reasoning about Z specifications. In: 3rd Northern Formal Methods Workshop, BCS Electronic Workshop in Computing (1998),

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Ian Toyn
    • 1
  • Andy Galloway
    • 1
  1. 1.Department of Computer ScienceUniversity of YorkHeslington, YorkUK

Personalised recommendations