David Lesens and Hassen Saïdi

Automatic Verification of Parameterized Networks of Processes by Abstraction.

To appear In Electronic Notes of Theoritical Computer Science (ENTCS) 1997. Revisited version of INFINITY'97.


Abstract

In this paper we are interested in the verification of safety properties of parameterized networks. A network is defined as a parallel composition of an arbitrary but finite number of identical sequential processes, where we consider parallel composition by interleaving and synchronization by shared variables. Using abstraction techniques, a process, called an {\it abstract network}, encoding the behavior of the entire network is constructed. The property is then checked on this process. Our verification method has the following advantages: the construction of the abstract network is fully automatic; the obtained process is generally a simple process on which the property can be easily verified. Of course, if the property cannot be verified on the abstract network, another weaker abstraction has to be computed. The construction requires to discharge a set of first order verification conditions (VCs). The PVS theorem prover is used to discharge the generated VCs. This allows us to consider processes with arbitrary data types. The effectiveness of our verification method is illustrated on two examples including a parameterized version of the Fischer's protocol.

Click here to get the postscript file of the full paper.

Click here to move to the web page describing our experimental results.