PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Gnesi S., Mazzanti F. On the fly model checking of communicating UML State Machines. The document has been submitted to Conference: VMCAI04-(Fifth International Conference on Verification, Model Checking and Abstract Interpretation), Technical report, 2003.
 
 
Abstract
(English)
In this paper we present an 'on the fly' model checker for the verification of the dynamic behavior of UML models seen as a set communicating state machines. The logic supported by the tool is an extension of the action based branching time temporal logic mu-actl and has the power of full mu-calculus. Early result on the application of this model checker to a case study have been also reported.
Subject UML
model checking
statechart diagrams
state machines
F.3.1 Specifying and Verifying and Reasoning about Programs
D.2.4 Software/Program Verification
68Q60, 03B70


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