PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Trentanni G. HAL (History Dependent Automata Laboratory) - online version.
 
 
Abstract
(English)
The HD-Automata Laboratory (HAL) is an integrated tool set for the specification, verification and analysis of concurrent and distributed systems. The core of HAL are the HD-automata: they are used as a common format for the various history-dependent languages. The HAL environment includes modules which implement decision procedures to calculate behavioral equivalences, and modules which support verification of behavioral properties expressed as formulae of suitable temporal logics. At this moment HAL works only with concurrent and distributed systems expressed by pi-calculus formalism. The HAL environment allows pi-calculus agents to be translated into ordinary automata, so that existing equivalence checkers can be used to calculate whether the pi-calculus are bisimilar. The environment also supports verification of logical formulae expressing desired properties of the behavior of pi-calculus agents.
URL: http://fmt.isti.cnr.it/hal/
Subject Process calculi, Automata
Bisimulation Verification
Pi-calculus, Location semantics
History preserving bisimulation
D.2.4 Software/Program Verification
D.2.5 Testing and Debugging



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