Formal Verification of Statemate-Statecharts

  • Kay Fuhrmann
  • Jan Hiemer
Conference paper
Part of the Advances in Computing Science book series (ACS)


During the software development process it is important to use powerful techniques for proving the expected behavior of the system and hence avoiding failures in real applications later on. Therefore, an effective means to increase confidence in the development process is to use analysis techniques based on the formal descriptions used in early phases (requirements specification).


Mutual Exclusion Linear Temporal Logic Finite State Automaton Verification Tool Copy Process 
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. [CL96]
    M. Conrad and E. Lehmann. Anforderungsspezifikation des Fahrgeschwindigkeitskonstanters mit Z und Statemate. Technischer Bericht Nr. F3S/K96–03,Daimler Benz AG, Berlin, 1996.Google Scholar
  2. [Emm90]
    E. A. Emmerson. Temporal and modal logic. Handbook of Theoretical Computer Science MIT Press, 1990.Google Scholar
  3. [For97]
    Formal Systems (Europe) Ltd. Failures Divergence Refinement, FDR2 User Manual, 1997.Google Scholar
  4. [Har87]
    D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8: 231–274, 1987.MathSciNetMATHCrossRefGoogle Scholar
  5. [HLN+90]
    David Harel, Hagi Lachover, Amnon Naamad, Amir Pnueli, Michal Politi, Rivi Sherman, Aharon Shtull-Trauring, and Mark Trakhtenbrot. Statemate: A working environment for the development of complex reactive systems. IEEE Transactions on Software Engineering, 16 No. 4, April 1990.Google Scholar
  6. [HN95]
    David Harel and Amnon Naamad. The stalemate semantics of statecharts. Technical Report, i-Logis, October 1995.Google Scholar
  7. [Hoa78]
    C.A.R. Hoare. Communicating sequential processes. Communications of the ACM, Number 8, 21: 666–667, 1978.Google Scholar
  8. [Hoa85]
    C.A.R. Hoare. CSP - Communicating Sequential Processes. Prentice Hall International, 1985.Google Scholar
  9. [Sca95]
    J.B. Scattergood. Tools for CSP and Timed CSP, D.Phil. Oxford University Computing Laboratory, 1995.Google Scholar

Copyright information

© Springer-Verlag Wien 1999

Authors and Affiliations

  • Kay Fuhrmann
    • 1
  • Jan Hiemer
    • 1
  1. 1.Research and TechnologyDaimler-BenzGermany

Personalised recommendations