We present methods and tools for the verification of behaviours of Lotos programs, based on the explicit construction of a finite automaton. We discuss a behaviour oriented style for Lotos that eases the construction of this model. We present the verification tools integrated in the lite tool set, and illustrate the approach with the full specification and analysis of a datagram protocol.
An exercise in protocol verification
Gnesi S;
1992
Abstract
We present methods and tools for the verification of behaviours of Lotos programs, based on the explicit construction of a finite automaton. We discuss a behaviour oriented style for Lotos that eases the construction of this model. We present the verification tools integrated in the lite tool set, and illustrate the approach with the full specification and analysis of a datagram protocol.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_453459-doc_172342.pdf
solo utenti autorizzati
Descrizione: An exercise in protocol verification
Tipologia:
Versione Editoriale (PDF)
Dimensione
3.81 MB
Formato
Adobe PDF
|
3.81 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.
