2003
Journal article
Restricted
A model-checking verification environment for mobile processes
Ferrari Gl, Gnesi S, Montanari U, Pistore M
Software Program Verification
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.
Source: ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, vol. 12, pp. 440-473
Back to previous page
BibTeX entry
@article{oai:it.cnr:prodotti:43909,
title = {A model-checking verification environment for mobile processes},
author = {Ferrari Gl and Gnesi S and Montanari U and Pistore M},
year = {2003}
}CNR authorsLaboratories
0000-0002-0139-0421