Model-Checking Techniques for Reliable Communication over Unreliable Media

Abstract

We present a simple approach to modeling and verification of the well-known Alternating Bit Protocol using the model checker UPPAAL to investigate different communication assumptions of the protocol, for instance that the messages can be lost or corrupted during the transmission. We verify safety and liveness properties of the protocol for reliable communication and ensure that the protocol satisfies these properties even in the case of message failures