Seminario Interdipartimentale di Algoritmica
 
 
 

Dipartimento di Informatica (ex-Scienze dell'Informazione) - D(S)I
via Salaria 113, piano terzo
Aula Seminari

Abstract:
(English) The main obstruction to automatic verification of Finite State Systems is the huge amount of memory required to complete the verification task at hand (state explosion). This motivates research on distributed as well as disk based verification algorithms.
After reviewing some basic notion about Explicit State Space Exploration we present a novel Disk Based Breadth First Explicit State Space Exploration algorithm as well as an implementation of it within the Murphi 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 Murphi 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) Murphi 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) Murphi with enough RAM memory to complete the verification task at hand.
Using our disk based Murphi 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 Murphi.

-- Work presented at FMCAD 2002, LNCS, Springer

(Italiano) L'ostruzione principale alla verifica automatica di sistemi a Stati Finiti e' la quantita' di memoria necessaria per completare la verifica (state explosion). Questo motiva la ricerca su algoritmi di verifica distribuiti o su memoria secondaria. Dopo una breve introduzione al model checking verra' presentato un nuovo algoritmo di verifica su memoria secondaria. Tale algoritmo e' stato implementato nel model checker Murphi. I nostri risultati sperimentali mostrano che, anche usando solo 1/10 della RAM necessaria per completare la verifica, il nostro algoritmo e' in media solo 3 volte piu' lento di "RAM Murphi" con abbastanza RAM per completare la verifica. Usando il nostro "Disk Murphi" siamo stati in grado di completare la verifica di un protocollo con circa $10^9$ stati. Questo richiederebbe piu' di 5 gigabytes di RAM usando "RAM Murphi".