Database of Case Studies Achieved Using CADP

Heuristic Search for Equivalence Checking

Organisation: University of Pisa and University of Sannio (ITALY)

Method: CCS
LOTOS

Tools used: CWB-NC
CADP (Construction and Analysis of Distributed Processes)

Domain: Concurrency Theory.

Period: 2014-2016

Size: n/a.

Description: 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.

Conclusions: 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. Quoting [DeFrancesco-Lettieri-Santone-Vaglini-16]:
    CADP uses very efficient algorithms, and great attention is devoted to implementation efficiency issues.


Publications: [DeFrancesco-Lettieri-Santone-Vaglini-16] 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 our FTP site in PDF or PostScript
Contact:
Prof. Nicoletta De Francesco
Dipartimento di Ingegneria dell'Informazione
University of Pisa
Via Diotisalvi, 2
I-56126 Pisa
ITALY
Tel: +39 (50) 2217527
Email: n.defrancesco@ing.unipi.it



Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Wed Mar 28 11:26:36 2018.


Back to the CADP case studies page