scientific article; zbMATH DE number 1544531
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.
- A compositional axiomatization of statecharts
- A constructive approach to state description semantics
- Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker
- A comparison of Statecharts step semantics
- Semantic specification and verification of data flow diagrams
- Translating SA/RT models to synchronous reactive systems: An approximation to modular verification using the SMV model checker
- Part-whole statecharts for precise behavioral semantics
- Invariant-based synthesis of fault-tolerant systems
- SVtL: System Verification Through Logic Tool Support for Verifying Sliced Hierarchical Statecharts
- Are Statecharts Finite Automata?
- scientific article; zbMATH DE number 4056977 (Why is no real title available?)
- scientific article; zbMATH DE number 1286822 (Why is no real title available?)
- Statecharts to specify the control of automated manufacturing systems
- scientific article; zbMATH DE number 522848 (Why is no real title available?)
- Transitions as interrupts: A new semantics for timed statecharts
- Compositional Verification of Quantitative Properties of Statecharts
- Formal verification of UML statecharts with real-time extensions
- Formal verification of STATEMATE-statecharts
- Semantics of full statecharts based on graph rewriting
- Computer Aided Verification
- Fundamental Approaches to Software Engineering
- Formal Techniques for Networked and Distributed Systems - FORTE 2005
- Theoretical Aspects of Computing - ICTAC 2004
- Equivalences of Statecharts
- A semantics for distributed execution of Statemate
- A formal semantics of extended hierarchical state transition matrices using CSP\#
- Verification of well-formed communicating recursive state machines
- Verification of scope-dependent hierarchical state machines
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4520893)
