PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Gnesi S., Mazzanti F. A Temporal Logic for UML Statecharts. The document Conference: FASE 2005, Technical report, 2004.
 
 
Abstract
(English)
In this paper we present 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 UML statecharts, branching time temporal logic
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