Parameterized Verification of Pi-Calculus Systems
In this paper we present an automatic verification technique for
parameterized systems where the subsystem behavior is modeled using the Pi
calculus. At its core, our technique treats each process instance in a
system as a property transformer. Given a property F that we want to verify
of a N-process system, we use a partial model checker to infer the property
F' (stated as a formula in a sufficiently rich logic) that must hold of an
(N-1)-process system. If the sequence of formulas F,F',..., thus constructed
converges, and the limit is satisfied by the zero process, we can conclude
that the N-process system satisfies F. In this paper we present a partial
model checker for the Pi-calculus that uses an expressive value-passing
logic as the property language. We also develop a number of optimizations
to make the model checker efficient enough for routine use, and a
light-weight widening operator to approximate the limit of a sequence of
formulas. We demonstrate the effectiveness of our technique by using it to
verify properties of a wide variety of parameterized systems that are beyond
the reach of existing techniques.