University of Pisa and University of Sannio (ITALY)
CADP (Construction and Analysis of Distributed Processes)
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. This work proposes
an equivalence checking method based on heuristic search techniques
on AND/OR graphs. A key assumption of heuristic search is that a
utility or cost can be assigned to each state to guide the search
by suggesting the next state to expand; in this way, the most
promising paths are considered first. The heuristic functions
are syntactically defined on the CCS process algebra.
The heuristic search equivalence checking method has been implemented (for strong and weak equivalence) in a prototype tool and compared with the equivalence checking implementations provided by CWB-NC and CADP on a number of case studies. Regarding strong equivalence, the heuristic search method outperforms the other tools, although CADP exhibits better time performance in some cases (e.g., for the MUTUAL case study). Regarding weak equivalence, while its memory occupation is higher, CADP shows a better performance in general.
Heuristic search proves to be a viable alternative in improving
the performance of equivalence checking. Experimental evidence
was provided of the reduction in both state space and running time
that may result when applying the heuristic search method
with respect to CWB-NC and CADP, when checking strong equivalence.
For weak equivalence, the performance of the heuristic search
method is lower than CADP in terms of analysis scalability,
and comparable with CADP in terms of memory space reduction.
N. De Francesco, G. Lettieri, A. Santone, and G. Vaglini.
"Heuristic Search for Equivalence Checking".
Software and Systems Modeling 15(2):513-530, May 2016.
Available on-line from https://www.researchgate.net/profile/Gigliola_Vaglini/publication/285414779_Heuristic_search_for_equivalence_checking/links/567293e208ae54b5e462b908/Heuristic-search-for-equivalence-checking.pdf
and from the VASY FTP site in PDF or PostScript
Prof. Nicoletta De Francesco
Dipartimento di Ingegneria dell'Informazione
University of Pisa
Via Diotisalvi, 2
Tel: +39 (50) 2217527
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|