Model checking UML Statechart diagrams using JACK

Author

Gnesi, Stefania ; Latella, Diego ; Massink, Mieke

Author_Institution

Istituto di Elaborazione dell´´Inf., CNR, Pisa, Italy

fYear

1999

fDate

1999

Firstpage

46

Lastpage

55

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;

fLanguage

English

Publisher

ieee

Conference_Titel

High-Assurance Systems Engineering, 1999. Proceedings. 4th IEEE International Symposium on

Conference_Location

Washington, DC

Print_ISBN

0-7695-0418-3

Type

conf

DOI

10.1109/HASE.1999.809474

Filename

809474