Formalizing statecharts using hierarchical automata
Article
Helke, S. and Kammueller, F. 2010. Formalizing statecharts using hierarchical automata. Archive of Formal Proof.
Type | Article |
---|---|
Title | Formalizing statecharts using hierarchical automata |
Authors | Helke, S. and Kammueller, F. |
Abstract | We formalize in Isabelle/HOL the abtract syntax and a synchronous step semantics for the specification language Statecharts. The formalization is based on Hierarchical Automata which allow a structural decomposition of Statecharts into Sequential Automata. To support the composition of Statecharts, we introduce calculating operators to construct a Hierarchical Automaton in a stepwise manner. Furthermore, we present a complete semantics of Statecharts including a theory of data spaces, which enables the modelling of racing effects. We also adapt CTL for Statecharts to build a bridge for future combinations with model checking. However the main motivation of this work is to provide a sound and complete basis for reasoning on Statecharts. As a central meta theorem we prove that the well-formedness of a Statechart is preserved by the semantics. |
Research Group | Foundations of Computing group |
Artificial Intelligence group | |
Journal | Archive of Formal Proof |
ISSN | 2150-914X |
Publication process dates | |
Deposited | 25 May 2012 |
Output status | Published |
Web address (URL) | http://afp.sourceforge.net/entries/Statecharts.shtml |
Language | English |
https://repository.mdx.ac.uk/item/83q4x
30
total views0
total downloads0
views this month0
downloads this month