|
SENSORIA All Publications |
|
Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
show main publications
A Model Checking Verification Environment for UML Statecharts
@INPROCEEDINGS{GnesiMazzantiAICA2005,
title = {{A Model Checking Verification Environment for UML Statecharts}},
author = {{Stefania} {Gnesi} and {Franco} {Mazzanti}},
booktitle = {Proceedings XLIII AICA Annual Conference, University of Udine - AICA 2005},
abstract = {In this paper we present the state/event-based temporal logic mu-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 mu-UCTL. The logic is supported by a prototypical verification environment under development at ISTI built around the on-the-fly UMC model checker.},
year = {2005},
url = {http://fmt.isti.cnr.it/WEBPAPER/gmaica2005.pdf},
month = {2-5 October},
partner = {ISTI},
status = {public},
task = {T3.3},
}
|
