Formal verification of a Cooperative Automatic Repeat reQuest MAC protocol

Cooperative communications, in which a relay node helps the source node to deliver its packets to the destination node, are able to obtain significant benefits in terms of transmission reliability, coverage extension and energy efficiency. A Cooperative Automatic Repeat reQuest (C-ARQ) MAC protocol has been recently proposed to exploit cooperative diversity at the MAC layer. In this paper, we validate the integrity and the validity of the C-ARQ protocol using formal methods. The protocol logic is modeled in SDL and implemented in PROMELA. The functionality of the C-ARQ protocol is verified through simulations and verifications using SPIN.

► A novel cooperative MAC protocol for wireless distributed networks, C-ARQ, is described with a formal SDL model. ► SPIN and PROMELA are used to verify the correctness and functionality of C-ARQ. ► Simulation results from SPIN coincide with the protocol description. ► The proposed cooperative communication property claim always holds true in verifications.