No label defined (Q4520893)

The work of E. Mikk is concerned with the semantics and verification of Statecharts, a graphical language for the specification of reactive systems proposed by David Harel in 1984. The formalism, which is historically classified in the synchronous language group, extends the usual graphical representation of fine state machine by means of state-transition diagrams, by allowing hierarchical structure on states, explicit representation of parallelism and communication among parallel. In the last decade a number of variants of Statecharts have been proposed in the literature. One of them is implemented in the commercial CASE tool Statemate. The PhD thesis focus on semantics and verification techniques for this variant of Statecharts. As semantics is concerned, the author proposes a formalization by means of Z notation of the semantics underlying Statemate (already rigorously described, even if in a different mathematical style, by D. Harel and A. Naamad). The relevant contributions of the work can be found in the part where verification of Statecharts is addressed. In order to implement tools for the verification of Statecharts, the author preliminarily devise a formalism, called Extended Hierarchical Automata (EHA), which restricts the syntax of Statecharts though allowing to easily capture the full formalism. With respect to the full syntax of Statecharts, EHA's avoid inter-level transitions, namely, transitions which do not respect the hierarchy on states (inter-level transitions, acting as a `goto' mechanism, prevent a clear decomposition of a statechart into sub-statecharts). An algorithm is provided which correctly translates Statecharts into EHA's. The correctness of the translations is proved by showing that the semantics of a statechart and the semantics of its translation (both of them given in terms of Labelled Transition Structures) are bisimilar. The formalism of EHA's plays the role of front-end for the implementation of verification tools. Verification is obtained by linking EHA's to two existing model checkers: SPIN which allow to describe properties to check by LTL (Linear Time Logic) formulas, and SMC (Symbolic Model Verifier), which allow to describe properties to check by CTL (Computation Tree Logic) formulas. The first verification tool is obtained by translating EHA's into Promela, the input specification language of SPIN. A second verification tool is obtained by translating EHA's into the input language of the model checker SMV. Both of the translations are proved to be correct in the sense that they preserve the semantics of EHA's upto bisimulation. As a result, the translations form Statecharts to SPIN and SMV (via EHA's) allow to check properties of Statecharts expressed by LTL and CTL formulas (since bisimulation preserves LTL and CTL properties). The work is concluded by a rich set of cases studies to convince that the proposed technique is suitable for practical verification.