In this paper we present an automatic verification technique for parameterized systems where the subsystem behavior is modeled using the π-calculus. At its core, our technique treats each process instance in a system as a property transformer. Given a property φ that we want to verify of an N-process system, we use a partial model checker to infer the property φ′ (stated as a formula in a sufficiently rich logic) that must hold of an (N - 1)-process system. If the sequence of formulas φ, φ′, . . . thus constructed converges, and the limit is satisfied by the deadlocked process, we can conclude that the N-process system satisfies φ. To this end, we develop a partial model checker for the π-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. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Yang, P., Basu, S., & Ramakrishnan, C. R. (2006). Parameterized verification of π-calculus systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3920 LNCS, pp. 42–47). Springer Verlag. https://doi.org/10.1007/11691372_3
Mendeley helps you to discover research relevant for your work.