In this paper we present a logic verification environment for mobile system specified by p-calculus terms. Properties of mobile system espressed by using an action-based temporal logic. Exploting a feature of the environment, we can generate finite state automata for a wide class of p-calculus agents, by preserving a notion of bisimulation equivalence. Hence, the formulae can be verified by applying a classical model check-in approach. In particular, we present as casa study, the verification of some propeties of a GSM protocol for mobile telephones, specified using a p-calculus.
Model checking a mobile telephone system
Gnesi S;
1997
Abstract
In this paper we present a logic verification environment for mobile system specified by p-calculus terms. Properties of mobile system espressed by using an action-based temporal logic. Exploting a feature of the environment, we can generate finite state automata for a wide class of p-calculus agents, by preserving a notion of bisimulation equivalence. Hence, the formulae can be verified by applying a classical model check-in approach. In particular, we present as casa study, the verification of some propeties of a GSM protocol for mobile telephones, specified using a p-calculus.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_409275-doc_143845.pdf
solo utenti autorizzati
Descrizione: Model checking a mobile telephone system
Tipologia:
Versione Editoriale (PDF)
Dimensione
611.94 kB
Formato
Adobe PDF
|
611.94 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.
