PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Gnesi S., Mazzanti F. A model checking framework for (Mobile) UML statecharts. In: Foundations of Global Computing (Schloss Dagstuhl, Wadern, Germany, 20/25/02 2005).
 
 
Abstract
(English)
In this paper we present an ``on the fly'' model checker for the verification of the dynamic behavior of UML models seen as a set of communicating state machines. The logic supported by the tool is the state/event-based temporal logic $muuctl$ that makes possible the description of properties on UML model evolutions and assertions on explicit local state variables of UML state machines. This logic allows both to specify the basic properties that a state should satisfy, and to combine these basic predicates with advanced logic or temporal operators. Doubly Labelled Transition Systems are the semantic domain for $muuctl$ where states are labelled by sets of propositions that hold in them and transitions by events performed. The logic we propose here is then applied to verify properties over the dynamic behaviour of a mobile system modelled as extended UML statecharts.
Subject Mobile UML statecharts
Model checking
Action/State based Temporal Logic
D.2.4 Software/Program Verification
F.3.1 Specifying and Verifying and Reasoning about Programs


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