基于CBMC有界模型检测的无线抄表路由协议验证

• 作者: 刘渊 杨红丽 王非 秦胜潮 胡世超
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: 模型检测 WM2RP路由协议 CBMC
• 年，卷（期）: 2016,（4）
• 所属期刊栏目: 网络与通信
• 页码范围: 138-142
• 页数: 5页
• 分类号: TP3
• 字数: 4432字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2016.04.033

摘要

针对工业界实现的无线抄表路由协议WM2RP(Wireless Meter Reading Routing Protocol),提出将CBMC有界模型检测工具运用到该协议实现的验证方法.WM2RP协议实现是嵌入式C程序,CBMC工具主要针对嵌入式软件的验证,运用CBMC对WM2RP进行验证十分适用.CBMC能够直接对C/C++源码进行验证,这样不仅省去了传统模型检测技术需要对代码抽象建模的工作,而且不用担心模型和代码之间可能存在的不一致性问题.首先利用CBMC系统自生成断言验证技术,找到WM2RP协议实现中可能存在的漏洞,并对实现协议的公司给予反馈.然后进一步借助CBMC提供的用户自定义断言技术,通过自定义断言的插入以及对实现代码的适当处理,验证了WM2RP协议的网络层接收函数实现与协议规范的相符性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	杨红丽	北京工业大学计算机学院	20	106	5.0	9.0
2	胡世超	北京工业大学计算机学院	2	7	2.0	2.0
3	秦胜潮	提赛德大学计算机学院	3	10	2.0	3.0
4	王非	北京工业大学计算机学院	4	15	3.0	3.0
5	刘渊		3	20	2.0	3.0