A Temporal Logic for UML Statecharts

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.