PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Mazzanti F. UMC User Guide (version 3.3). Technical report, 2006.
 
 
Abstract
(English)
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.
Subject D.2.4 Software/Program Verification
F.3.1 Specifying and Verifying and Reasoning about Programs


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