HAL (History dependant Automata Laboratory) - online version [Release 1.2]

Gnesi S., Pistore M., Trentanni G.

Model Checking  Formal verification  Mobile Systems  Equivalences 

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-dependant 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.