Title :
Model checking UML Statechart diagrams using JACK
Author :
Gnesi, Stefania ; Latella, Diego ; Massink, Mieke
Author_Institution :
Istituto di Elaborazione dell´´Inf., CNR, Pisa, Italy
Abstract :
Statechart diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modelling Language (UML). In this paper, we present a branching-time model-checking approach to the automatic verification of the formal correctness of UML Statechart diagram specifications. We use a formal operational semantics for building a labelled transition system (automaton) which is then used as a model to be checked against correctness requirements expressed in Action-Based Temporal Logic (ACTL). Our reference verification environment is JACK, where automata are represented in a standard format, which facilitates the use of different tools for automatic verification
Keywords :
automata theory; computer aided software engineering; diagrams; formal specification; formal verification; specification languages; temporal logic; ACTL; Action-Based Temporal Logic; JACK; UML Statechart diagram specifications; Unified Modelling Language; automatic verification; automaton; branching-time model-checking approach; correctness requirements; dynamic system behaviour; formal correctness; formal operational semantics; graphical notation; labelled transition system; verification environment; Algebra; Automata; Contracts; Formal verification; Graphics; LAN interconnection; Logic functions; Unified modeling language; Visualization;
Conference_Titel :
High-Assurance Systems Engineering, 1999. Proceedings. 4th IEEE International Symposium on
Conference_Location :
Washington, DC
Print_ISBN :
0-7695-0418-3
DOI :
10.1109/HASE.1999.809474
