2003
Journal article  Unknown

A model-checking verification environment for mobile processes

Ferrari G. L., 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 12 (2003): 440–473.

Publisher: Association for Computing Machinery,, New York, NY , Stati Uniti d'America



Back to previous page
BibTeX entry
@article{oai:it.cnr:prodotti:43909,
	title = {A model-checking verification environment for mobile processes},
	author = {Ferrari G. L. and Gnesi S. and Montanari U. and Pistore M.},
	publisher = {Association for Computing Machinery,, New York, NY , Stati Uniti d'America},
	journal = {ACM transactions on software engineering and methodology},
	volume = {12},
	pages = {440–473},
	year = {2003}
}