Formalizing statecharts using hierarchical automata

摘要: We formalize in Isabelle/HOL the abtract syntax and a synchronous step semantics for specification language Statecharts. The formalization is based on Hierarchical Automata which allow structural decomposition of Statecharts into Sequential Automata. To support composition Statecharts, we introduce calculating operators to construct Automaton stepwise manner. Furthermore, present complete including theory data spaces, enables modelling racing effects. also adapt CTL build bridge future combinations with model checking. However main motivation this work provide sound basis reasoning As central meta theorem prove that well-formedness Statechart preserved by semantics. (Abstract as appears publisher website)