[isabelle] New AFP entry: Formalizing Statecharts using Hierarchical Automata

Steffen Helke and Florian Kammüller

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.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.