Istituto di Scienza e Tecnologie dell'Informazione     
Gnesi S., Mazzanti F. A model checking verification environment for UML statecharts. In: AICA 2005 (Udine, 5-7 Ottobre 2005). Atti, 2005.
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.
URL: http://matrix.isti.cnr.it/~mazzanti/publications/aica2005.pdf
Subject Software/Program Verification
D.2.4 Software/Program Verification

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