CNR Institutional Research Information System

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.

HAL (History Dependent Automata Laboratory) - online version [Release 1.0]

Gnesi S;Trentanni G
2002

Abstract

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.
2002
Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo" - ISTI
Inglese
Codice PuMa: cnr.isti/2002-SW-002 - Bibliografia di riferimento: * Montanari, U. and Pistore, M., Checking Bisimilarity for Finitary pi-calculus, in: Insup Lee, Scott A. Smolka, Eds., CONCUR'95: Concurrency Theory, Springer LNCS 962, pp. 42-56. * Montanari, U., Pistore, M., and Yankelevich, D., Efficient Minimization up to Location Equivalence, in: Hanne Riis Nielson, Ed., Programming Languages and Systems - ESOP'96, Springer LNCS 1058, pp. 265-279. * Montanari, U. and Pistore, M., History Dependent Verification for Partial Order Systems, in: D. Peled, V.Pratt, and G. Holzmann, Eds., Procs. Partial Order Methods in Verifications, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol.29, 259-272, 1996. * Montanari, U. and Pistore, M., Minimal Transition Systems for History-Preserving Bisimulation, in: Ruediger Reischuk, Michel Morvan, Eds., STACS 97, Springer LNCS 1200, 1997, pp. 413-425. Paper available from file: ftp://ftp.di.unipi.it/pub/Papers/pistore/stacs97.ps.gz. * Ferrari, G., Ferro, G., Gnesi, S., Montanari, U., Pistore, M. and Ristori, G., An Automata Based Verification Environment for Mobile Processes, in: Ed Brinksma, Ed., Tools and Algorithms for the Construction and Analysis of Systems, Springer LNCS 1217, 1997, pp. 275-289. * Ferrari, G., Gnesi, S., Montanari, U., Pistore, M. and Ristori, G., Verifying Mobile Processes in the HAL Environment, in: Alan J. Hu and Moshe Y. Vardi, Eds., CAV'98, Springer LNCS 1427, pp.511-515. * Montanari, U. and Pistore, M., An Introduction to History Dependent Automata, in: Andrew Gordon, Andrew Pitts and Carolyn Talcott, Eds, Second Workshop on Higher-Order Operational Techniques in Semantics (HOOTS II), ENTCS, Vol. 10, 1998, Paper available from file: http://www.elsevier.nl/cas/tree/store/tcs/free/entcs/store/tcs10/cover.sub.sht. * Montanari, U. and Pistore, M., Finite State Verification for the Asynchronous Pi-Calculus, in: W. Rance Cleaveland, Ed., TACAS'99, Springer LNCS 1579, pp.255-269, 1999. * Montanari, U. and Pistore, M., Pi-Calculus, Structured Coalgebras and Minimal HD-Automata, in: Mogens Nielsen and Branislav Roman, Eds., Proc. MFCS 2000, Springer LNCS 1983. * Ferrari, G., Montanari, U. and Pistore, M., Minimizing Transition Systems for Name Passing Calculi: A Co-algebraic Formulation, in: Mogens Nielsen and Uffe Engberg, Eds., FOSSACS 2002, Springer LNCS 2303, pp.129-143. * Buscemi, M. and Montanari, U., A First Order Coalgebraic Model of Pi-Calculus Early Observational Equivalence, Proc. CONCUR 2002, Springer LNCS, to appear. * Montanari, U. and Pistore, M., History-Dependent Automata, Technical Report TR-98-11, Dipartimento di Informatica, Pisa. Draft available from file: ftp://ftp.di.unipi.it/pub/Papers/pistore/hdaut.ps.gz. * Montanari, U. and Pistore, M., Structured Coalgebras and Minimal HD-Automata for the pi-Calculus, Technical Report 0006-02, IRST-ITC, 2000. Paper available from file: http://sra.itc.it/paper.epl?id=MP00.
Process calculi
Automata
Bisimulation
Verification
Pi-calculus
Location semantics
History preserving bisimulation
http://fmt.isti.cnr.it:8080/hal/
3
Gnesi, S; Pistore, M; Trentanni, G
296
none
05 Altro::05.11 Software
info:eu-repo/semantics/other
05.11 Software
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.14243/330121
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact