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.