• Complex
  • Title
  • Keyword
  • Abstract
  • Scholars
  • Journal
  • ISSN
  • Conference
搜索

Author:

胡世超 (胡世超.) | 杨红丽 (杨红丽.) | 秦胜潮 (秦胜潮.) | 王非 (王非.) | 刘渊 (刘渊.)

Indexed by:

CQVIP CSCD

Abstract:

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

Keyword:

模型检测 WM2RP路由协议 CBMC

Author Community:

  • [ 1 ] [胡世超]北京工业大学
  • [ 2 ] [杨红丽]北京工业大学
  • [ 3 ] [秦胜潮]提赛德大学计算机学院 英国米德尔斯堡
  • [ 4 ] [王非]北京工业大学
  • [ 5 ] [刘渊]西安普瑞米特科技有限公司 陕西西安710075

Reprint Author's Address:

Email:

Show more details

Related Keywords:

Related Article:

Source :

计算机应用与软件

ISSN: 1000-386X

Year: 2016

Issue: 4

Volume: 33

Page: 138-142

Cited Count:

WoS CC 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: 1

Affiliated Colleges:

Online/Total:424/5439434
Address:BJUT Library(100 Pingleyuan,Chaoyang District,Beijing 100124, China Post Code:100124) Contact Us:010-67392185
Copyright:BJUT Library Technical Support:Beijing Aegean Software Co., Ltd.