Institutional Repository
| formal verification on distributed spectrum sensing protocol | |
| Liu Jin-Bo; Liao Ming-Xue; Hu Xiao-Hui; He Xiao-Xin | |
| 2011 | |
| Conference Name | 2011 International Conference on Computer Science and Network Technology, ICCSNT 2011 |
| Source | Proceedings of 2011 International Conference on Computer Science and Network Technology, ICCSNT 2011 |
| Pages | 190-194 |
| Conference Date | December 24, 2011 - December 26, 2011 |
| Conference Place | Harbin, China |
| Indexed Type | EI ; ISTP |
| ISBN | 9781457715846 |
| Department | (1) National Key Laboratory of Science and Technology on Integrated Information System Technology Institute of Software Chinese Academy of Sciences Beijing China |
| English Abstract | 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. © 2011 IEEE.; 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. © 2011 IEEE. |
| Keyword | Computer Science Global System For Mobile Communications Quality Of Service Wireless Networks Wireless Telecommunication Systems |
| Sponsorship | IEEE |
| Subject | Computer Science ; Engineering |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16288 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Liu Jin-Bo,Liao Ming-Xue,Hu Xiao-Hui,et al. formal verification on distributed spectrum sensing protocol[C],2011:190-194. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment