A modular approach to protocol verification using process algebra

Summary

A version of the Alternating Bit Protocol is verified by means of process algebra. To avoid a combinatorial explosion, a notion of ‘modules’ is introduced and the protocol is divided in two such modules. A method is developed for verifying conglomerates of modules and applied to the motivating example.

One of the basic problems in protocol verification is the following: data are to be transmitted from A to B via some unreliable medium M. A protocol has been proposed for doing so correctly and perhaps efficiently. A rigorous mathematical proof of the correctness claim is desired.

Now protocol verification aims at providing the techniques for giving such a proof. Several formalisms have been advocated, but as yet none has been widely accepted.

The framework we adhere to is process algebra. The first protocol correctness proof by means of process algebra is in Bergstra and Klop, where a simple version of the Alternating Bit Protocol is verified.

We have tried our hands at a more complicated version, called the Concurrent Alternating Bit Protocol (CABP) and found that the number of possible state transitions was prohibitively large. In this article we propose a divide-and-conquer strategy. We group processes into modules, describe and verify their behaviour and finally combine them. For different approaches, see.

In Section 1 we deal with the Concurrent Alternating Bit Protocol (CABP). In Section 2 we present the modular approach. Modules are introduced in Section 3, whereas the verification of the CABP is given in Section 4.