UMC User Guide (version 3.3)
Mazzanti F.
Software requirements analysis
In this report we present the prototypical UMC verification tool under development at ISTI. UMC accept a system specification given in UML-like style as a collection of active objects, modelled by state-machines, and whose behavior is described through statecharts. On such systems UMC allows to verify properties specified in the mu-UCTL logic: a temporal logic which enriches the full mu-calculus with the more abstract (and weak) CTL/ACTL like temporal operators, and with a rich set of state propositions and ACTL action expressions. Both the basic comand-line oriented tool (umc) and its more user-friendly web-based interface are presented. This web interface integrates also verification functionalities provided by the other environments (EST, FC2TOOLS) which allow system abstraction and minimization.
Source: ISTI Technical reports, 2006
Back to previous page
@techreport{oai:it.cnr:prodotti:160363,
title = {UMC User Guide (version 3.3)},
author = {Mazzanti F.},
institution = {ISTI Technical reports, 2006},
year = {2006}
}
0000-0003-4562-8777