Verification of Parameterized Pi-Calculus Systems

parameterized system consists of a number of instances of a component, the number of such occurrences being the parameter to the system. Many safety-critical systems are naturally parameterized: e.g. resource arbitration protocols, communication protocols, etc. While traditional model checking techniques can be used to verify properties of an instance of a parameterized system (for a specific value of the parameter), many novel techniques have been developed to verify such systems for all instances of their parameters. These techniques vary in the classes of systems they can handle and the degree of automation they provide. The automatic techniques typically restrict the communication topology (e.g. rings or trees) or, at least, demand that the communication patterns be fixed. We have developed an automatic verification technique for parameterized mobile systems where the subsystem behavior is modeled using the pi-calculus. The technique is based on a compositional model checker that considers a system comprising a process and an environment, and computes the obligation on the environment for a given property to hold in the system. We have also developed a number of optimizations to make the model checker efficient enough for routine use.