Sciweavers

HASE
1999
IEEE

Model Checking UML Statechart Diagrams Using JACK

13 years 8 months ago
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.
Stefania Gnesi, Diego Latella, Mieke Massink
Added 03 Aug 2010
Updated 03 Aug 2010
Type Conference
Year 1999
Where HASE
Authors Stefania Gnesi, Diego Latella, Mieke Massink
Comments (0)