|
28th Annual Conference on Current
Trends in
Theory and Practice of Informatics
|
|
November 24 - December 1, 2001
|
|
Model Checking for Communication Protocols
by Pablo Argon, Giorgio Delzanno, Supratik Mukhopadhyay, Andreas Podelski
Abstract:
Brand and Zafiropulo [BZ83] introduced the model of communicating
finite-state machines to represent a distributed system connected with FIFO
channels. Several different communication protocols can be specified with this
simple model. In this paper we address the problem of automatically validating
protocols by verifying properties such as well-formedness and absence of
deadlock. Our method is based on a representation of communicating finite-state
machines in terms of logic programs. This leads to efficient verification
algorithms based on the ground and non-ground semantics of logic programming.