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 of communicating state machines. The logic supported by the tool is an extension of the action based branching time temporal logic m-ACTL and has the power of full m-calculus. Early results on the application of this model checker to a case study have been also reported.
On the fly model checking of communicating UML state machines
Gnesi S;Mazzanti F
2004
Abstract
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 of communicating state machines. The logic supported by the tool is an extension of the action based branching time temporal logic m-ACTL and has the power of full m-calculus. Early results on the application of this model checker to a case study have been also reported.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_91092-doc_125491.pdf
solo utenti autorizzati
Descrizione: On the fly model checking of communicating UML State Machines
Tipologia:
Versione Editoriale (PDF)
Dimensione
240.76 kB
Formato
Adobe PDF
|
240.76 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
