Constraint-Based Verification of Client-Server Protocols
We show that existing constraint manipulation technology incorporated in the paradigm of symbolic model checking with rich assertional languages [KMM+97], can be successfully applied to the verification of client-server protocols with a finite but unbounded number of clients. Abstract interpretation is the mathematical bridge between protocol specifications and the constraint-based verification method on heterogeneous data used in the Action Language Verifier, a model checker for CTL [BYK01]. The method we propose is incomplete but fully automatic and sound for safety and liveness properties. Suficient conditions for termination of the resulting procedures can be derived by using the theory of [ACJT96]. As a case-study, we apply the method to check safety and liveness properties for a formal model of Steve German’s directory based consistency protocol [PRZ01].
KeywordsModel Check Safety Property Liveness Property Symbolic Model Check Exclusive Access
Unable to display preview. Download preview PDF.
- [ACJT96]P. A. Abdulla, K. Cerāns, B. Jonsson and Y.-K. Tsay. General Decidability Theorems for Infinite-State Systems. In Proc. LICS’ 99, pp. 313–321, 1996.Google Scholar
- [BCR01]T. Ball, S. Chaki, S. K. Rajamani. Parameterized Verification of Multithreaded Software Libraries. In Proc. TACAS’ 01, LNCS 2031, pp. 158–173, 2001.Google Scholar
- [Bul00]T. Bultan. Action Language: A specification language for model checking reactive systems. In Proc. ICSE’ 00, pp. 335–344, 2000.Google Scholar
- [BYK01]T. Bultan and T. Yavuz-Kahveci. Action Language Verifier. In Proc. ASE’ 01, 2001.Google Scholar
- [CC77]P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. POPL’ 77 pp. 238–252, 1977.Google Scholar
- [CGP99]E. M. Clarke, O. Grumberg, D. Peled. Model Checking. MIT Press, December 1999.Google Scholar
- [CUDD]Fabio Somenzi. CUDD: the CU Decision Diagram Package, Release 2.3.1. http://vlsi.colorado.edu/~fabio/cudd/.
- [Del00]G. Delzanno. Automatic Verification of Parameterized Cache Coherence Protocols. In Proc. CAV’ 00, LNCS 1855, pp. 53–68, 1996.Google Scholar
- [DEP99]G. Delzanno, J. Esparza, and A. Podelski. Constraint-based Analysis of Broadcast Protocols. In Proc. CSL’ 99, LNCS 1683, pp. 50–66, 1999.Google Scholar
- [DP99]G. Delzanno, A. Podelski. Model Checking in CLP. In Proc. TACAS’ 99, LNCS 1579, pp. 223–239, 1999.Google Scholar
- [EN98]E. A. Emerson and K. S. Namjoshi. On Model Checking for Nondeterministic Infinite-state Systems. In Proc. LICS’ 98, pp. 70–80, 1998.Google Scholar
- [EFM99]J. Esparza, A. Finkel, and R. Mayr. On the Verification of Broadcast Protocols. In Proc. LICS’ 99, pp. 352–359, 1999.Google Scholar
- [Fri00]L. Fribourg. Constraint Logic Programming Applied to Model Checking. In Proc. LOPSTR’ 99, LNCS 1817, pp. 30–41, 1999.Google Scholar
- [Ger00]S.M. German. Personal communication.Google Scholar
- [Hal93]N. Halbwachs. Delay Analysis in Synchronous Programs. In Proc. CAV’ 93, LNCS 697, pp. 333–346, 1993.Google Scholar
- [Hol88]G. Holzmann Algorithms for Automated Protocol Verification. AT&T Technical Journal 69(2):32–44, 1988.Google Scholar
- [KMP+95]W. Kelly, V. Maslov, W. Pugh, E. Rosser, T. Shpeisman, and D. Wonnacott. The Omega library interface guide. Technical Report CS-TR-3445, Department of Computer Science, University of Maryland, College Park, March 1995. See also http://www.cs.umd.edu/projects/omega/.
- [KMM+97]Y. Kesten, O. Maler, M. Marcus, A. Pnueli, E. Shahar. Symbolic Model Checking with Rich Assertional Languages. In Proc. CAV’ 97, pp. 424–435, 1997.Google Scholar
- [McM93]K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, 1993.Google Scholar
- [PRZ01]A. Pnueli, S. Ruah, L. D. Zuck Automatic Deductive Verification with Invisible Invariants. In Proc. TACAS’ 01, LNCS 2031, pp. 82–97, 2001.Google Scholar
- [YKTB01]T. Yavuz-Kahveci, M. Tuncer, and T. Bultan. A Library for Composite Symbolic Representations. In Proc. TACAS’ 01, LNCS 2031, pp. 52–66, 2001.Google Scholar