A timed semantics for the StateMate implementation of statecharts

  • Carsta Petersohn
  • Luis Urbina
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1313)


The two central simulation algorithms of the StateMate tool for Statecharts are formalized following the most recent description by Harel and Naamad [7]. Our semantics is given in terms of fair and clocked transition systems [15, 12]. The main benefit from providing such formal semantics is that analysis tools developed for these transition systems can now be applied to StateMate specifications. We also discuss typical properties of synchronous languages for our semantics.


Transition System Formal Semantic Action Expression Internal Clock State Hierarchy 
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.
    R. Alur and D. L. Dill. A Theory of Timed Automata. Theoretical Computer Science, 126:183–235, 1994.Google Scholar
  2. 2.
    A. Benveniste and G. Berry. The Synchronous Approach to Reactive and Real-Time Systems. Proceedings of IEEE, 79(9):1270–1282, 1991.Google Scholar
  3. 3.
    G. Berry and G. Gonthier. The Esterel Synchronous Programming Language: Design, Semantics, Implementation. Science of Computer Programming, 19(2):87–152, 1992.Google Scholar
  4. 4.
    D. Harel. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming, 8:231–274, 1987.CrossRefGoogle Scholar
  5. 5.
    D. Harel and E. Gery. Executable Object Modeling with Statecharts. In 18th ICSE, Berlin, 1996.Google Scholar
  6. 6.
    D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. ShtullTrauring, and M. Trakhtenbrot. Statemate: A Working Environment for the Development of Complex Reactive Systems. IEEE Transaction on Software Engineering, 16(4):403–414, 1990.CrossRefGoogle Scholar
  7. 7.
    D. Harel and A. Naamad. The STATEMATE Semantics of Statecharts. ACM Transaction on Software Engineering and Methodology, 5(4):292–333, 1996.Google Scholar
  8. 8.
    D. Harel and A. Pnueli. On the Development of Reactive Systems. In Logics and Models of Concurrent Systems, pages 477–498. Springer-Verlag, 1985.Google Scholar
  9. 9.
    D. Harel, A. Pnueli, J. Schmidt, and R. Sherman. On the Formal Semantics of Statecharts. In LICS'87, pages 54–64. Computer Society Press, 1987.Google Scholar
  10. 10.
    J. Helbig and P. Kelb. An OBDD-Representation of Statecharts. In EDAC'94, pages 142–149, 1994.Google Scholar
  11. 11.
    C. Huizing and R. T. Gerth. Semantics of Reactive Systems in Abstract Time. In Real-Time: Theory in Practice, LNCS 600, pages 291–314. Springer-Verlag, 1991.Google Scholar
  12. 12.
    Y. Kesten, Z. Manna, and A. Pnueli. Verifying Clocked Transition Systems. In Hybrid Systems III, LNCS 1066, pages 13–40. Springer-Verlag, 1996.Google Scholar
  13. 13.
    Y. Kesten and A. Pnueli. Timed and Hybrid Statecharts and their Textual Representation. In FTRTFT'92, LNCS 571, pages 591–619. Springer-Verlag, 1992.Google Scholar
  14. 14.
    A. Maggiolo-Schettini and A. Peron. Retiming Techniques for Statecharts. In FTRTFT'96, LNCS 1135, pages 55–71, 1996.Google Scholar
  15. 15.
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems, volume 1. Springer-Verlag, 1992.Google Scholar
  16. 16.
    F. Maraninchi and N. Halbwachs. Compositional Semantics of Non-deterministic Synchronous Languages. In ESOP'96, LNCS 1058. Springer-Verlag, 1996.Google Scholar
  17. 17.
    A. Pnueli and M. Shalev. What is in a Step: On Semantics of Statecharts. In TACS'91, LNCS 526, pages 244–264. Springer-Verlag, 1991.Google Scholar
  18. 18.
    A.C. Uselton and S.A. Smolka. A Process Algebraic Semantics for Statecharts via State Refinement. In PROCOMET'94, IFIP, pages 262–281, 1994.Google Scholar
  19. 19.
    M. von der Beeck. A Comparison of Statecharts Variants. In FTRTFT'94, LNCS 863, pages 128–148. Springer-Verlag, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Carsta Petersohn
    • 1
  • Luis Urbina
    • 1
  1. 1.Institut fur Informatik and Praktische MathematikChristian-Albrechts-Universität KielKielGermany

Personalised recommendations