Model checking communication protocols

Abstract

Brand and Zafiropulo [1] 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.