Equivalence checking plays a crucial role in formal verification since it is a natural relation for expressing the matching of a system implementation against its specification. In this paper, we present an efficient procedure, based on heuristic search, for checking well-known bisimulation equivalences for concurrent systems specified through process algebras. The method tries to improve, with respect to other solutions, both the memory occupation and the time required for proving the equivalence of systems. A prototype has been developed to evaluate the approach on several examples of concurrent system specifications.
Heuristic search for equivalence checking
DE FRANCESCO, NICOLETTA;LETTIERI, GIUSEPPE;VAGLINI, GIGLIOLA
2016-01-01
Abstract
Equivalence checking plays a crucial role in formal verification since it is a natural relation for expressing the matching of a system implementation against its specification. In this paper, we present an efficient procedure, based on heuristic search, for checking well-known bisimulation equivalences for concurrent systems specified through process algebras. The method tries to improve, with respect to other solutions, both the memory occupation and the time required for proving the equivalence of systems. A prototype has been developed to evaluate the approach on several examples of concurrent system specifications.File | Dimensione | Formato | |
---|---|---|---|
Francesco2016_Article_HeuristicSearchForEquivalenceC.pdf
solo utenti autorizzati
Tipologia:
Versione finale editoriale
Licenza:
NON PUBBLICO - Accesso privato/ristretto
Dimensione
1.19 MB
Formato
Adobe PDF
|
1.19 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
santone.pdf
Open Access dal 02/05/2017
Tipologia:
Documento in Post-print
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
496.67 kB
Formato
Adobe PDF
|
496.67 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.