Abstract
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.
This research was supported in part by NSF grants CCR-0205376, CCR-0311512, and CCR 0509340.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Henzinger, T.: Reactive modules. In: LICS (1996)
Alur, R., Madhusudan, P., Nam, W.: Symbolic compositional verification by learning assumptions. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 548–562. Springer, Heidelberg (2005)
Andersen, H.R.: Partial model checking (extended abstract). In: LICS (1995)
Andersen, H.R., Stirling, C., Winskel, G.: A compositional proof system for the modal mu-calculus. In: LICS (1994)
Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 221. Springer, Heidelberg (2001)
Basu, S., Ramakrishnan, C.R.: Compositional analysis for verification of parameterized systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 315–330. Springer, Heidelberg (2003)
Berezin, S., Gurov, D.: A compositional proof system for the modal mu-calculus and CCS. Technical Report CMU-CS-97-105, CMU (1997)
Bradfield, J., Stirling, C.: Modal logics and mu-calculi: an introduction (In the Handbook of Process Algebra), pp. 293–330. Elsevier, Amsterdam (2001)
Chaki, S., Rajamani, S.K., Rehof, J.: Types as models: model checking mes-sage-passing programs. In: Proceedings of POPL, pp. 45–57 (2002)
Clarke, E.M., Grumberg, O., Jha, S.: Verifying parameterized networks. ACM Transactions on Programming Languages and Systems (1997)
Dam, M.: Proof systems for pi-calculus logics. Logic for Concurrency and Synchronisation (2001)
Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, p. 582. Springer, Heidelberg (2000)
Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: POPL (1995)
Emerson, E.A., Namjoshi, K.S.: Automated verification of parameterized synchronous systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, p. 472. Springer, Heidelberg (1996)
Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite state systems. In: LICS (1998)
Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS (1999)
Cleaveland, R., Bhat, G.: Efficient model checking via the equational ì-calculus. In: LICS, pp. 304–312 (1996)
Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems (1994)
Henzinger, T., Qadeer, S., Rajamani, S.K.: You assume, we guarantee. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, p. 552. Springer, Heidelberg (1998)
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)
Igarashi, A., Kobayashi, N.: A generic type system for the pi-calculus. Theoretical Computer Science 311(1–3), 121–163 (2004)
Ip, C.N., Dill, D.L.: Verifying systems with replicated components in murphi. Formal Methods in System Design (1999)
Kesten, Y., Pnueli, A.: Control and data abstraction:the cornerstones of pratical formal verification. International Journal on Software tools for Technology (2000)
Kozen, D.: Results on the propositional ì-calculus. Theoretical Computer Science (1983)
Lin, H.: Symbolic bisimulation and proof systems for the ð-calculus. Technical report, School of Cognitive and Computer Science, U. of Sussex, UK (1994)
McMillan, K.L.: Compositional rule for hardware design refinement. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, Parts I and II. Information and Computation 100(1), 1–77 (1992)
Orava, F., Parrow, J.: An algebraic verification of a mobile network. Journal of Formal Aspects of Computing 4, 497–543 (1992)
Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisi-ble invariants. In: Tools and Algorithms for the Construction and Analysis of Systems (2001)
Pnueli, A., Shahar, E.: Liveness and acceleration in parameterized verification. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)
Song, H., Compton, K.J.: Verifying pi-calculus processes by Promela trans-lation. Technical Report CSE-TR-472-03, Univ. of Michigan (2003)
Victor, B.: TheMobility Workbench user’s guide. Technical report, Department of Computer Systems, Uppsala University, Sweden (1995)
Yang, P., Basu, S., Ramakrishnan, C.R.: Parameterized verification of π-calculus systems (2006), http://www.lmc.cs.sunysb.edu/~pyang/ptech.pdf
Yang, P., Ramakrishnan, C.R., Smolka, S.A.: A logical encoding of the π-calculus: Model checking mobile processes using tabled resolution. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 116–131. Springer, Heidelberg (2002)
Yang, P., Ramakrishnan, C.R., Smolka, S.A.: A provably correct compiler for efficient model checking of mobile processes. In: Proceedings of PADL (2005)
Zuck, L., Pnueli, A.: Model checking and abstraction to the aid of param-eterized systems (a survey). Computer Languages, Systems & Structures 30(3–4), 139–169 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yang, P., Basu, S., Ramakrishnan, C.R. (2006). Parameterized Verification of π-Calculus Systems. In: Hermanns, H., Palsberg, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2006. Lecture Notes in Computer Science, vol 3920. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691372_3
Download citation
DOI: https://doi.org/10.1007/11691372_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33056-1
Online ISBN: 978-3-540-33057-8
eBook Packages: Computer ScienceComputer Science (R0)