8th IEEE Asia-Pacific Software Engineering Conference (APSEC),
4-7 December 2001, Macau SAR, China

Paper Title:
A Probabilistic Approach to  Automatic Verification 
of Concurrent Systems

Authors:

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

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

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

Marisa Venturini Zilli
Area Informatica, 
Universit\`a di L'Aquila, 
Coppito 67100, L'Aquila, Italy
email: zilli@dsi.uniroma1.it




Abstract

The main obstruction to automatic verification of
{\em concurrent systems}
is the huge amount of memory required to complete the verification
task ({\em state explosion}).

In this paper we present a probabilistic algorithm 
for {\em automatic verification} via {\em model checking}.
Our algorithm trades space with time.
In particular, when our memory is over because of state explosion
our algorithm does not give up verification. 
Instead it just proceeds at a {\em lower speed}
and its results will only hold with some {\em arbitrarily small}
error probability.

Our preliminary experimental results show that 
using our probabilistic algorithm we can typically save 
more than 30\% of RAM with an average time penalty of about 100\%
w.r.t. a deterministic state  space exploration with enough 
memory to complete the verification task.
This is better than having to give up the verification task
because of lack of memory.




Keywords:
Concurrent Systems, Distributed Systems, Reactive Systems,
Embedded Systems, Formal Methods, Automatic Verification and Validation,
Model Checking, Probabilistic Verification.