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.