A Complete Protocol Verification using Relativized Bisimulation

K.G. Larsen and R. Milner

Abstract: The purpose of this paper is to illustrate a compositional proof method for communicating systems; that is, a method in which a property p of a complete system is demonstrated by first decomposing the system, then demonsrating properties of the subsystems which are strong enough to entail property p for the complete system. In any compositional proof method, it is essential that one can express the behavioural constraint which is imposed upon each subsystem by the others, since it may be difficult to demonstrate a suitable property of the subsystem's behaviour in the absence of the constraint.

Our method is an extension of the well established notion of bisimulation; it is called relative bisimulation, and was developed specifically to express the behavioural constraints between subsystems. We illustrate the method in a proof of correctness for a version of the Alternating Bit Protocol.

LFCS report ECS-LFCS-86-13

Previous | Index | Next