| dc.contributor.author | He, Xin | |
| dc.contributor.author | Kumar, Ram | |
| dc.contributor.author | Mu, Liping | |
| dc.contributor.author | Gjøsæter, Terje | |
| dc.contributor.author | Li, Frank Y. | |
| dc.date.accessioned | 2012-08-20T10:16:36Z | |
| dc.date.available | 2012-08-20T10:16:36Z | |
| dc.date.issued | 2012 | |
| dc.identifier.citation | He, 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 | no_NO |
| dc.identifier.issn | 0920-5489 | |
| dc.identifier.uri | http://hdl.handle.net/11250/137951 | |
| dc.description | 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 | no_NO |
| dc.description.abstract | 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. | no_NO |
| dc.language.iso | eng | no_NO |
| dc.publisher | Elsevier | no_NO |
| dc.subject | cooperative communications | no_NO |
| dc.subject | finite model-checking | no_NO |
| dc.subject | protocol verification | no_NO |
| dc.subject | PROMELA | no_NO |
| dc.title | Formal verification of a Cooperative Automatic Repeat reQuest MAC protocol | no_NO |
| dc.type | Journal article | no_NO |
| dc.type | Peer reviewed | no_NO |
| dc.subject.nsi | VDP::Mathematics and natural science: 400::Information and communication science: 420::Algorithms and computability theory: 422 | no_NO |
| dc.source.pagenumber | 343-354 | no_NO |
| dc.source.volume | 34 | no_NO |
| dc.source.journal | Computer Standards & Interfaces | no_NO |
| dc.source.issue | 4 | no_NO |
