Uniform Verification of Parameterized Networks

Amir Pnueli

The John von Neumann Minerva Center for Verification of Reactive Systems

Weizmann Institute of Science

A parameterized network is a system consisting of many interconnected processes, whose size is a parameter. A typical example is a set of processes situated on a ring whose size is a parameter N. Usually, each individual process in the network is a finite-set program communicating with its close neighbors. We can always verify properties of particular instances of such a network, e.g. consider a process-ring of sizes 5, 7, and 11, by automatic model-checking techniques. However this is not in general sufficient in order to conclude that the properties are valid over ALL instances of the system. Uniform verification of such systems attempts to establish in one verification effort the validity of the considered properties for EVERY value of the parameter N. In the talk, we will survey several approaches to the solution of this problem. The three approaches to be reviewed are the formation of Network Invariants, Finitary Abstraction, and Regular Symbolic Model-Checking, which performs symbolic model checking over a rich assertional language which can capture infinite sets of states.

Last modified: Wed Apr 26 15:21:49 MET DST 2000