TY  - CONF
AU  - Della Penna, Giuseppe
AU  - Intrigila, Benedetto
AU  - Tronci, Enrico
AU  - Venturini Zilli, Marisa
ED  - Aagaard, M.
ED  - O'Leary, J.W.
PY  - 2002
DA  - 2002//
TI  - Exploiting Transition Locality in the Disk Based Mur$\varphi$ Verifier
BT  - 4th International Conference on Formal Methods in Computer-Aided Design (FMCAD)
T3  - Lecture Notes in Computer Science
SP  - 202
EP  - 219
VL  - 2517
PB  - Springer
CY  - Portland, OR, USA
AB  - The main obstruction to automatic verification of Finite State Systems is the huge amount of memory required to complete the verification task (state explosion). This motivates research on distributed as well as disk based verification algorithms. In this paper we present a disk based Breadth First Explicit State Space Exploration algorithm as well as an implementation of it within the Mur$\varphi$ verifier. Our algorithm exploits transition locality (i.e. the statistical fact that most transitions lead to unvisited states or to recently visited states) to decrease disk read accesses thus reducing the time overhead due to disk usage. A disk based verification algorithm for Mur$\varphi$ has been already proposed in the literature. To measure the time speed up due to locality exploitation we compared our algorithm with such previously proposed algorithm. Our experimental results show that our disk based verification algorithm is typically more than 10 times faster than such previously proposed disk based verification algorithm. To measure the time overhead due to disk usage we compared our algorithm with RAM based verification using the (standard) Mur$\varphi$ verifier with enough memory to complete the verification task. Our experimental results show that even when using 1/10 of the RAM needed to complete verification, our disk based algorithm is only between 1.4 and 5.3 times (3 times on average) slower than (RAM) Mur$\varphi$ with enough RAM memory to complete the verification task at hand. Using our disk based Mur$\varphi$ we were able to complete verification of a protocol with about $10^9$ reachable states. This would require more than 5 gigabytes of RAM using RAM based Mur$\varphi$.
SN  - 3-540-00116-6
L1  - http://mclab.di.uniroma1.it/publications/papers/papers/Della Penna2002.pdf
UR  - https://doi.org/10.1007/3-540-36126-X_13
DO  - 10.1007/3-540-36126-X_13
N1  - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=41), last updated on Sat, 24 Nov 2012 14:28:28 +0100
ID  - DellaPenna_etal2002
ER  -