zbMATH — the first resource for mathematics

Constraint-based verification of client-server protocols. (English) Zbl 1067.68624
Walsh, Toby (ed.), Principles and practice of constraint programming - CP 2001. 7th international conference, Paphos, Cyprus, November 26 – December 1, 2001. Proceedings. Berlin: Springer (ISBN 3-540-42863-1). Lect. Notes Comput. Sci. 2239, 286-301 (2001).
Summary: We show that existing constraint manipulation technology incorporated in the paradigm of symbolic model checking with rich assertional languages 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. The method we propose is incomplete but fully automatic and sound for safety and liveness properties. Sufficient conditions for termination of the resulting procedures can be derived by using the theory of P. A. Abdulla, K. Čerāns, B. Jonsson, and Y.-K. Tsay, [\`\` General decidability theorems for infinite-state systems”, in: 11th Annual IEEE Symposium on Logic in Computer Science (New Brunswick, NJ, 1996), 313–321, IEEE Comput. Soc. Press, Los Alamitos, CA (1996)]. 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.
For the entire collection see [Zbl 0984.00059].

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: Link