收录：
摘要：
针对工业界实现的无线抄表路由协议WM2RP(Wireless Meter Reading Routing Protocol),提出将CBMC有界模型检测工具运用到该协议实现的验证方法。WM2RP协议实现是嵌入式C程序,CBMC工具主要针对嵌入式软件的验证,运用CBMC对WM2RP进行验证十分适用。CBMC能够直接对C/C++源码进行验证,这样不仅省去了传统模型检测技术需要对代码抽象建模的工作,而且不用担心模型和代码之间可能存在的不一致性问题。首先利用CBMC系统自生成断言验证技术,找到WM2RP协议实现中可能存在的漏洞,并对实现协议的公司给予反馈。然后进一步借助CBMC提供的用户自定义断言技术...
关键词：
通讯作者信息：
电子邮件地址：
