PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Ferrari G., Gnesi S., Montanari U., Pistore M. A model checking verification environment for mobile systems. The document has been submitted to Journal: ACM TOSEM, Technical report, 2003.
 
 
Abstract
(English)
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
Subject Pi-calculus
mobile systems
model checking
D.2.4 Software/Program Verification . Formal methods . Model checking


Icona documento 1) Download Document PS


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