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.
A model checking framework for (Mobile) UML statecharts
Gnesi S;Mazzanti F
2005
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
