Hierarchical automata as model for statecharts

Extended abstract
  • Erich Mikk
  • Yassine Lakhnechi
  • Michael Siegel
Session 4
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1345)


Statecharts are a very rich graphical specification formalism supported by the commercial tool Statemate. Statecharts comprises powerful concepts such as interlevel transitions, multiple-source/multiple-target transitions, priority amongst transitions and simultaneous execution of maximal non-conflicting sets of transitions. Every add-on tool which is supposed to be linked with the Statemate tool have to deal with the rather involved semantics of these concepts. We propose extended hierarchical automata as an intermediate format to facilitate the linking of new tools to the Statemate environment, whose main idea is to devise a simple formalism with a more restricted syntax than statecharts which nevertheless allows to capture the richer formalism. We define the format, give operational semantics to it, and translate statecharts to it.


Operational Semantic Linear Temporal Logic Parallel Composition Composition Function Kripke Structure 
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. [Har87]
    D. Harel. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming, 8:231–274, 1987.CrossRefGoogle Scholar
  2. [HdR91]
    C. Huizing and W.-P. de Roever. Introduction to design choices in the semantics of Statecharts. Information Processing Letters, 37:205–213, February 1991.CrossRefGoogle Scholar
  3. [HK94]
    J. Helbig and P. Kelb. An OBDD-Representation of Statecharts. In Proc. of the European Design and Test Conference EDAC'94, pages 142–149, 1994.Google Scholar
  4. [HN96]
    D. Harel and A. Naamad. The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology, 5(4):293–333, Oct 1996.CrossRefGoogle Scholar
  5. [Hol91]
    G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, New Jersey, 1991.Google Scholar
  6. [Hol97]
    G.J. Holzmann. The Model Checker Spin. IEEE Trans. on Software Engineering, 23(5):279–295, May 1997. Special issue on Formal Methods in Software Practice.CrossRefGoogle Scholar
  7. [HP94]
    G.J. Holzmann and D. Peled. An improvement in formal verification. In Proc. FORTE94, Berne, Switzerland, October 1994.Google Scholar
  8. [Hui91]
    C. Huizing. Semantics of reactive systems: comparision and full abstraction. PhD thesis, Technical University Eindhoven, 1991.Google Scholar
  9. [JM94]
    F. Jahanian and A. Mok. Modechart: a specification language for real-time systems. IEEE Transactions of Software Engineering, 20(12):933–947, December 1994.CrossRefGoogle Scholar
  10. [LHHR94]
    N.G. Leveson, M.P.E. Heimdahl, H. Hildreth, and J.D. Reese. Requirements Specification for Process-Control Systems. IEEE Trans. Soft Eng, 20(9):684–707, September 1994.CrossRefGoogle Scholar
  11. [LL95]
    C. Lewerentz and T. Lindner. Formal Development of Reactive Systems: Case Study Production Cell. Number 891 in LNCS. Springer Verlag, 1995.Google Scholar
  12. [Mar91]
    F. Maraninchi. The Argos language: Graphical Representation of Automata and Description of Reactive Systems. In IEEE Workshop on Visual Languages, Oct 1991.Google Scholar
  13. [Mar92]
    F. Maraninchi. Operational and Compositional Semantics of Synchronous Automaton Compositions. In CONCUR'92, number 630 in Lecture Notes in Computer Science, pages 550–564. Springer-Verlag, 1992.Google Scholar
  14. [MHLS97]
    E. Mikk, G. J. Holzmann, Y. Lakhnech, and M. Siegel. Implementing Statecharts in Promela/SPIN. Technical report, Manuscript, 1997.Google Scholar
  15. [MLPS97]
    E. Mikk, Y. Lakhnech, C. Petersohn, and M. Siegel. On formal semantics of Statecharts as supported by Statemate. In 2nd BCS-FAGS Northern Formal Methods Workshop. Springer-Verlag, July 97.Google Scholar
  16. [NVG91]
    S. Narayan, F. Vahid, and D. D. Gajski. System Specification and Synthesis with the SpecCharts Language. In Proceedings, 1991 IEEE International Conference on Computer-Aided Design (ICCAD '91), pages 266–269, November 11–14 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Erich Mikk
    • 1
  • Yassine Lakhnechi
    • 1
  • Michael Siegel
    • 2
  1. 1.Christian-Albrechts-Universität zu KielInstitut für Informatik and Praktische MathematikKielGermany
  2. 2.Department of Applied Mathematics and Computer ScienceWeizmann Institute of ScienceRehovotIsrael

Personalised recommendations