# Formalizing Statecharts using Hierarchical Automata

 Title: Formalizing Statecharts using Hierarchical Automata Authors: Steffen Helke (helke /at/ cs /dot/ tu-berlin /dot/ de) and Florian Kammüller (flokam /at/ cs /dot/ tu-berlin /dot/ de) Submission date: 2010-08-08 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. BibTeX: @article{Statecharts-AFP, author = {Steffen Helke and Florian Kammüller}, title = {Formalizing Statecharts using Hierarchical Automata}, journal = {Archive of Formal Proofs}, month = aug, year = 2010, note = {\url{https://isa-afp.org/entries/Statecharts.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License