PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Ferrari G., Gnesi S., Montanari U., Pistore M. A model-checking verification environment for mobile processes. In: Acm Transactions on Software Engineering and Methodology, vol. Volume 12 (Issue 4 (October 2003)) pp. 440 - 473. ACM, 2003.
 
 
Abstract
(English)
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.
Subject Software
Program Verification
F.3.1 Specifying and Verifying and Reasoning about Programs


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional