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] |
C. R. Ramakrishnan
(cram@cs.sunysb.edu)