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