A model-checking verification environment for mobile processes
Gian-Luigi Ferrari, Stefania Gnesi, Ugo Montanari, Marco Pistore · ACM Transactions on Software Engineering and Methodology · 2003
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.