formal verification on distributed spectrum sensing protocol | |
Liu Jin-Bo ; Liao Ming-Xue ; Hu Xiao-Hui ; He Xiao-Xin | |
2011 | |
会议名称 | 2011 International Conference on Computer Science and Network Technology, ICCSNT 2011 |
会议日期 | December 24, 2011 - December 26, 2011 |
会议地点 | Harbin, China |
关键词 | Computer science Global system for mobile communications Quality of service Wireless networks Wireless telecommunication systems |
页码 | 190-194 |
中文摘要 | 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. |
收录类别 | EI ; ISTP |
会议主办者 | IEEE |
会议录 | Proceedings of 2011 International Conference on Computer Science and Network Technology, ICCSNT 2011 |
学科主题 | Computer Science ; Engineering |
语种 | 英语 |
ISBN号 | 9781457715846 |
内容类型 | 会议论文 |
源URL | [http://ir.iscas.ac.cn/handle/311060/16288] |
专题 | 软件研究所_软件所图书馆_会议论文 |
推荐引用方式 GB/T 7714 | Liu Jin-Bo,Liao Ming-Xue,Hu Xiao-Hui,et al. formal verification on distributed spectrum sensing protocol[C]. 见:2011 International Conference on Computer Science and Network Technology, ICCSNT 2011. Harbin, China. December 24, 2011 - December 26, 2011. |
个性服务 |
查看访问统计 |
相关权益政策 |
暂无数据 |
收藏/分享 |
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。
修改评论