Title: Exploiting Transition Locality in Automatic Verification

Authors:

Enrico Tronci
Area Informatica, Universit\`a di L'Aquila,
Coppito 67100, L'Aquila, Italy
tronci@univaq.it
http://univaq.it/~tronci

Giuseppe Della Penna
Area Informatica, Universit\`a di L'Aquila,
Coppito 67100, L'Aquila, Italy
gdellape@univaq.it

Benedetto Intrigila
Area Informatica, Universit\`a di L'Aquila,
Coppito 67100, L'Aquila, Italy
intrigil@univaq.it

Marisa Venturini Zilli
Dip. di Scienze dell'Informazione,
Universit\`a di Roma ``La Sapienza'',
Via Salaria 113, 00198 Roma, Italy
zilli@dsi.uniroma1.it


Abstract

The main obstruction to automatic verification of {\em Finite State Systems}
is the huge amount of memory required to complete the verification
task ({\em state explosion}).
In this paper we present an algorithm to contrast {\em state explosion}
when using  {\em Explicit State Space Exploration} to verify 
protocols.

We show experimentally that protocols exhibit {\em transition locality}.
That is, w.r.t. levels of a Breadth First (BF) visit,
state transitions tend to be between states belonging to
close levels of the transition graph.
We support our claim by measuring transition locality for the
set of protocols included in the Mur$\varphi$ verifier distribution.
To carry out our experiments we modified the Mur$\varphi$ verifier
so as to fit our needs.

We present a verification algorithm that exploits transition locality
as well as an implementation of it within the Mur$\varphi$ verifier.
Essentially, our algorithm replaces the hash table used in a BF
state exploration with a cache memory (i.e. visited states may be forgotten) 
and uses  disk storage for the BF queue.

Our algorithm is compatible with all (BF) optimization techniques
present in the Mur$\varphi$ verifier and it is by no means 
a substitute for any of them.
In fact, since our algorithm trades space with time,
it is typically most useful when one runs out of memory
and has already used all other state reduction techniques
present in the Mur$\varphi$ verifier. 

Our experimental results show that 
using our approach we can typically save more than 40\% of RAM
with an average time penalty of about 50\% when using (Mur$\varphi$)
bit compression and 100\% when using bit compression and hash compaction.

Shortly, our cache based approach typically
allows automatic verification of  systems more than 40\% larger 
than those that can be handled using a hash table based approach.



In:

Proceedings of: 11th Advanced Research Working Conference on
{\em Correct Hardware Design and Verification Methods} (CHARME),
4-7 September 2001, Livingston-Edinburgh (Scotland), LNCS, Springer-Verlag

Co-sponsored by the IFIP TC10/WG10.5 Working Group on:
Design and Engineering of Electronic Systems