Formal verification of a Cooperative Automatic Repeat reQuest MAC protocol
Journal article, Peer reviewed
MetadataShow full item record
Original versionHe, X., Kumar, R., Mu, L., Gjøsæter, T., & Li, F. Y. (2012). Formal verification of a Cooperative Automatic Repeat reQuest MAC protocol. Computer Standards & Interfaces, 34(4), 343-354. doi: 10.1016/j.csi.2011.12.001
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.
Author's version of an article published in the journal: Computer Standards & Interfaces. Also available from the publisher at: http://dx.doi.org/10.1016/j.csi.2011.12.001