This article presents a semantic-based environment for reasoning about the behavior of mobile systems. The verification environment, called HAL, exploits a novel automata-like model that allows finite-state verification of systems specified in the ?-calculus. The HAL system is able to interface with several efficient toolkits (e.g. model-checkers) to determine whether or not certain properties hold for a given specification. We report experimental results on some case studies.
A model-checking verification environment for mobile processes
Gnesi S;
2003
Abstract
This article presents a semantic-based environment for reasoning about the behavior of mobile systems. The verification environment, called HAL, exploits a novel automata-like model that allows finite-state verification of systems specified in the ?-calculus. The HAL system is able to interface with several efficient toolkits (e.g. model-checkers) to determine whether or not certain properties hold for a given specification. We report experimental results on some case studies.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_43909-doc_123095.pdf
solo utenti autorizzati
Descrizione: A model-checking verification environment for mobile processes
Tipologia:
Versione Editoriale (PDF)
Dimensione
557.91 kB
Formato
Adobe PDF
|
557.91 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.
