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.
  author  = {Steffen Helke and Florian Kammüller},
  title   = {Formalizing Statecharts using Hierarchical Automata},
  journal = {Archive of Formal Proofs},
  month   = aug,
  year    = 2010,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.