In this paper a semantic-based environment for reasoning about the behaviour of mobile systems is presented. The verification environment, called HAL, exploits a novel automata-like model which allows finite state verification of systems specified in the pi-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 with some case studies
A model checking verification environment for mobile systems
Gnesi S;
2003
Abstract
In this paper a semantic-based environment for reasoning about the behaviour of mobile systems is presented. The verification environment, called HAL, exploits a novel automata-like model which allows finite state verification of systems specified in the pi-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 with some case studiesFile in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
