Model Checking UML Statechart Diagrams Using JACK

Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modeling Language (UML). In this paper we present a branching time model-checking approach to the automatic verification of formal correctness of UML Statechart Diagrams specifications. We use a formal operational semantics for building a labeled transition system (automaton) which is then used as a model to be checked against correctness requirements expressed in the action based temporal logics 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.

• Type: Conference
• Year: 1999
• Where: HASE
• Authors: Stefania Gnesi, Diego Latella, Mieke Massink
• Keywords: Automatic Verification, Control Systems, HASE 1999, Statechart Diagrams, UML Statechart Diagrams