scientific article; zbMATH DE number 1286822
Since their introduction by David Harel statecharts have gained fast and widespread recognition, and have reviewed the interest in graphical specification methods. This work links statecharts to a second visual formalism, Rainer Schlör's symbolic timing diagrams, allowing to verify properties expressed in terms of timing diagrams, as a declarative language, about the behavioural dynamics of a reactive system that is specified in terms of statecharts, as an operational language. The proof system is compositional, complete, and, by contrast to existing approaches decidable; composition corresponds to conjunction. Although the presentation is quite formal -- in fact the present volume may be considered a single extensive proof of soundness and completeness of the axiom system -- our original objective was rather in practical applicability than in succinctness of the theoretical framework. Most of our early syntactical and semantical choices can be motivated this way, as for instance, a rather demanding composition structure for statecharts. The work sprung off (though was not part of) the Esprit project FORMAT, which provides an environment for the efficient development and formal verification of system-level VHDL designs, integrating declarative as well as operational language paradigms for both graphical and textual specification and implementation. Due to a notion of event and progress in time that is unified with that of VHDL, our intended statechart semantics will not employ full synchrony, but similar to the semantics supported by Kelb and commercially available statechart design tools as STATEMATE, where the events generated by a step only become visible with the next instant in time. We do however, allow inter-level transition, which we still feel somewhat essential to the original idea of hi-graphs; as it turns out they don't do any real harm, although they will render some of the proofs quite more involved. (This is by no means to imply that we consider these choices to be essential, neither to statecharts nor to our work.) The most important practical aspect, widening the range of automated verification tools that can be employed, is perhaps decidability, which is a consequence of the fact that symbolic timing diagrams correspond to linear time propositional temporal logic. The work consists of three parts. Part I presents the axiom system and provides a small example of how it might be used. Part II introduces the underlying statecharts semantics, in as intuitive terms as possible, first only for finished statecharts to facilitate comparison to conventional approaches, Own for statecharts that may remain subject to future refinement. The third part establishes soundness and completeness.
- Statecharts: a visual formalism for complex systems
- A compositional axiomatization of statecharts
- Timing diagrams: Formalization and algorithmic verification
- Visual specifications for modular reasoning about asynchronous systems
- Formalizing timing diagrams as causal dependencies for verification purposes
- Transitions as interrupts: A new semantics for timed statecharts
- scientific article; zbMATH DE number 1544531 (Why is no real title available?)
- Compositional Verification of Quantitative Properties of Statecharts
- Formal verification of STATEMATE-statecharts
- Proof tactics for a theory of state machines in a graphical environment
- Diagrammatic Representation and Inference
- A graphic language based on timing diagrams
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 Q4243082)
