PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Gnesi S., Latella D., Massink M. Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking. In: Journal of Logic and Algebraic Programming, vol. 51 pp. 43 - 75. Elsevier Science Inc, 2002.
 
 
Abstract
(English)
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.
Subject Formal specification
Formal semantics
Formal verification
Model-checking
UML
ACTL
JACK
D.2.4 Software/Program Verification


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional