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

News

july 28 2002

The HAL package is downloadable. You can download the last version of the HAL Environment here or test the online version here.


Slides

A first order coalgebraic model of pi-calculus early observational equivalence [Marzia Buscemi] [pdf]

From co-algebraic specification to verification environment [Gianluigi Ferrari] [pdf]

History Dependent Automata [Ugo Montanari] [pdf]

History Dependent Automata [Marco Pistore] [pdf]

History Dependent Automata: a Co- Algebraic definition, a Partitioning Algorithm and its Implementation [Roberto Raggi, Emilio Tuosto] [pdf]

Ongoing activity

  • Extensions for other semantics and calculi (open and weak semantics, fusion, spi...)
  • Optimization of the CAML implementation.
  • Compiler from pi-calculus term to HD-automata
  • Integration with the other tools (HAL, STA, Mobility Workbench)
  • Support for FC2 and XML file formats.
  • Web-services for on-line access (Profundis).

People



Case studies

Papers

History Dependent Automata [Abstract] [PDF] [Gzipped PS]

Minimizing Transition Systems for Name Passing Calculi:
A co-algebraic formulation [Abstract] [PDF] [Gzipped PS]

HD-Reducer Whitepaper [Abstract] [PDF] [Gzipped PS]

Bibliography

links

Profundis
Last modified on: November 27, 2003