Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking

Statechart diagrams provide a graphical notation to model dynamic aspects of system behaviour within the unified modelling language (UML). In this paper, we present a formal operational semantics for a behavioural subset of UML statechart diagrams (UMLSDs) including a formal proof of their correctness with respect to major UML semantics requirements concerning behavioural issues. We show how the modularity of our semantics definition can be exploited to define extensions, in particular we show an extension to models composed of collections of communicating statechart diagrams, which we call multicharts. Finally we present all the conceptual issues related to building a tool for action based branching time model-checking, for the automatic verification of formal correctness of UML multicharts. The approach we propose preserves all the information necessary to report the results of model-checking in terms of the original UMLSD specification. The reference verification environment used for this model-checking approach is JACK, where automata are represented in a standard format which facilitates the use of a collection of tools for automatic verification.