会议专题

Formal Verification on Distributed Spectrum Sensing Protocol

Wireless networks will provide much more convenience for mobile users via heterogeneous wireless architectures and dynamic spectrum access techniques. However, wireless networks also impose challenges on developers due to unknowing global electromagnetic environment information in each node, as well as diverse QoS requirements of various applications. Therefore, both correctness and reliability of communication protocol become extremely difficult In years, model checking has been advertised as a way to ensure the correctness of complex protocols. In this paper, we present a formal approach of formalizing and verifying a distributed wireless communication protocol used for cooperative spectrum sensing. Lots of well-defined properties are then verified for the protocol model. By using the model checker SPIN, we have discovered some vulnerabilities in the protocol, which can make some nodes trapped into either false liveness or zombie status.

component formal verification SPIN spectrum sensing protocol model checking distributed system

Jin-bo Liu Ming-xue Liao Xiao-hui Hu Xiao-xin He

National Key Laboratory of Science and Technology on Integrated Information System Technology, Insti National Key Laboratory of Science and Technology on Integrated Information System Technology, Insti

国际会议

2011 International Conference on Computer Science and Network Technology(2011计算机科学与网络技术国际会议 ICCSNT 2011)

哈尔滨

英文

190-194

2011-12-24(万方平台首次上网日期,不代表论文的发表时间)