A Bounded Retransmission Protocol for Large Data Packets: A Case Study in Computer Checked Algebraic Verification

Abstract

This note describes a protocol for the transmission of data packets that are too large to be transferred in their entirety. Therefore, the protocol splits the data packets and broadcasts it in parts. It is assumed that in case of failure of transmission through data channels, only a limited number of retries are allowed (bounded retransmission). If repeated failure occurs, the protocol stops trying and the sending and receiving protocol users are informed accordingly. The protocol and its external behaviour are specified in μCRL. The correspondence between these is shown using the axioms of μCRL. The whole proof of this correspondence has been computer checked using the proof checker Coq. This provides an example showing that proof checking of realistic protocols is feasible within the setting of process algebras.