Model checking UML statecharts diagrams using JACK

Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unied Modeling Language (UML). In this paper we present a branching time model-checking approach to the automatic verication of formal correctness of UML State-chart Diagrams specications. We use a formal operational semantics for building a la-beled transition system (automaton) which is then used as a model to be checked against correctness requirements ex-pressed in the action based temporal logics ACTL. Our ref-erence verication environment is JACK, where automata are represented in a standard format, which facilitates the use of different tools for automatic verication. 1