Hierarchical automata as model for statecharts
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.
KeywordsOperational Semantic Linear Temporal Logic Parallel Composition Composition Function Kripke Structure
Unable to display preview. Download preview PDF.
- [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
- [Hol91]G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, New Jersey, 1991.Google Scholar
- [HP94]G.J. Holzmann and D. Peled. An improvement in formal verification. In Proc. FORTE94, Berne, Switzerland, October 1994.Google Scholar
- [Hui91]C. Huizing. Semantics of reactive systems: comparision and full abstraction. PhD thesis, Technical University Eindhoven, 1991.Google Scholar
- [LL95]C. Lewerentz and T. Lindner. Formal Development of Reactive Systems: Case Study Production Cell. Number 891 in LNCS. Springer Verlag, 1995.Google Scholar
- [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
- [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
- [MHLS97]E. Mikk, G. J. Holzmann, Y. Lakhnech, and M. Siegel. Implementing Statecharts in Promela/SPIN. Technical report, Manuscript, 1997.Google Scholar
- [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
- [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