Indexed by：
Abstract：
针对工业界实现的无线抄表路由协议WM2RP(Wireless Meter Reading Routing Protocol),提出将CBMC有界模型检测工具运用到该协议实现的验证方法.WM2RP协议实现是嵌入式C程序,CBMC工具主要针对嵌入式软件的验证,运用CBMC对WM2RP进行验证十分适用.CBMC能够直接对C/C++源码进行验证,这样不仅省去了传统模型检测技术需要对代码抽象建模的工作,而且不用担心模型和代码之间可能存在的不一致性问题.首先利用CBMC系统自生成断言验证技术,找到WM2RP协议实现中可能存在的漏洞,并对实现协议的公司给予反馈.然后进一步借助CBMC提供的用户自定义断言技术,通过自定义断言的插入以及对实现代码的适当处理,验证了WM2RP协议的网络层接收函数实现与协议规范的相符性.
Keyword：
Reprint Author's Address：
Email：
Source ：
计算机应用与软件
ISSN： 1000-386X
Year： 2016
Issue： 4
Volume： 33
Page： 138-142
Cited Count：
SCOPUS Cited Count：
ESI Highly Cited Papers on the List： 0 Unfold All
WanFang Cited Count： 2
Chinese Cited Count：
30 Days PV： 4
Affiliated Colleges：
