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.
Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking
Gnesi S;Latella D;Massink M
2002
Abstract
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.File | Dimensione | Formato | |
---|---|---|---|
prod_43723-doc_56095.pdf
solo utenti autorizzati
Descrizione: Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking
Tipologia:
Versione Editoriale (PDF)
Dimensione
397.71 kB
Formato
Adobe PDF
|
397.71 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.