In this paper we present a prototypal environment to analyse LOTOS specifications, based on the integration between Squiggles, an equivalence verifier, and EMC, a model cheker for CTL formulae. Hence, the functionalities of our environment range from the reduction of a finite state LOTOS specification into its corresponding Labelled Transition System, possibly minimized with respect to an equivalence relation, to the verification of equivalence between specifications and to the check of validity of properties expressed in a temporal logic as CTL.
Model checking for LOTOS
Fantechi A;Gnesi S;
1991
Abstract
In this paper we present a prototypal environment to analyse LOTOS specifications, based on the integration between Squiggles, an equivalence verifier, and EMC, a model cheker for CTL formulae. Hence, the functionalities of our environment range from the reduction of a finite state LOTOS specification into its corresponding Labelled Transition System, possibly minimized with respect to an equivalence relation, to the verification of equivalence between specifications and to the check of validity of properties expressed in a temporal logic as CTL.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_447139-doc_161076.pdf
solo utenti autorizzati
Descrizione: Model checking for LOTOS
Tipologia:
Versione Editoriale (PDF)
Dimensione
1.85 MB
Formato
Adobe PDF
|
1.85 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
