A model checking verification environment for UML statecharts

In this paper we present the state/event-based temporal logic µUCTL which is a logic oriented towards a natural description of dynamic properties of UML models. This logic allows to specify the basic properties that a runtime system configuration should satisfy and to combine these basic predicates with logic and temporal operators which allow to take into consideration also the events performed by the system when evolving from one system configuration to another. Doubly Labelled Transition Systems are the semantic domain for µUCTL. The logic is supported by a prototypical verification environment under development at ISTI built around the 'on the fly' UMC model checker.