Parameterized Verification of Pi-Calculus Systems

Ping Yang, Samik Basu, C. R. Ramakrishnan


Abstract:

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 P that we want to verify of an N-process system, we use a partial model checker to infer the property P' (stated as a formula in a sufficiently rich logic) that must hold of an (N-1)-process system. If the sequence of formulas P, P', ... thus constructed converges, and the limit is satisfied by the deadlocked process, we can conclude that the N-process system satisfies P. To this end, we develop 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 accelerate convergence. 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.


Bibtex Entry:

@inproceedings{YBR:TACAS06,
author = {Ping Yang and  Samik Basu and  C. R. Ramakrishnan},
title = {Parameterized Verification of Pi-Calculus Systems},
booktitle = {12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS})},
address = {Vienna, Austria},
month = {Apr},
series = {Lecture Notes in Computer Science},
volume = {3920},
publisher = {Springer},
pages = {42--57},
year = {2006}
}


Full Paper: [pdf]


Home | Papers

C. R. Ramakrishnan
(cram@cs.sunysb.edu)