ROS中XML-RPC协议实现的形式化验证
文献类型：期刊论文
| 作者 | 贾娟娟 ; 施智平 ; 关永 ; 李勇坚 ; 魏洪兴 |
| 刊名 | 小型微型计算机系统
 |
| 出版日期 | 2015 |
| 卷号 | 36期号:12页码:2629-2633 |
| 关键词 | ROS系统 XML-RPC协议 有界模型检测 定理证明 |
| ISSN号 | 1000-1220 |
| 其他题名 | Formal Verification of XML-RPC Protocol in ROS |
| 中文摘要 | XML-RPC协议是ROS节点通讯的核心调用机制,其实现的正确性关乎整个系统的顺利运行. 使用模型检测和定理证明结合的方法对ROS系统中的XML-RPC协议进行验证. 首先使用CBMC模型检测工具逐个验证协议源代码的函数,然后对模型检测不能全面验证的循环结构使用霍尔逻辑建立模型并在Isabelle /HOL定理证明器中验证. 本文的工作结合两种形式化方法的优点,既克服了定理证明人工干预过多、工作量繁杂的问题,又避免了模型检测中出现状态爆炸的问题. |
| 英文摘要 | XML-RPC protocol is the core of the invocation mechanism in ROS system. The correctness of the protocol implementation is crucial to the ROS system Operate safely. This paper presents properties validation of XML-RPC protocol in ROS system with the method of model checking and theorem proving. Our work exploits the cooperation of Bounded model checking and theorem proving, to show the correctness of XML-RPC protocol,implemented CBMC and with respect to the loop structure that it cannot fully validated in CBMC,formalized in Isabelle /HOL. The paper has demonstrated a successful application of the linkage between theorem proving and model checking in a proof that takes advantage of the strengths of the respective proof assistants. This not only can overcome the problems occurring in the theorem proving,but also can avoid the emergence of model checking. |
| 收录类别 | CSCD |
| 语种 | 中文 |
| CSCD记录号 | CSCD:5588641 |
| 公开日期 | 2016-12-09 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/17384]  |
| 专题 | 软件研究所_软件所图书馆_期刊论文 |
| 推荐引用方式 GB/T 7714 | 贾娟娟,施智平,关永,等. ROS中XML-RPC协议实现的形式化验证[J]. 小型微型计算机系统,2015,36(12):2629-2633. |
| APA | 贾娟娟,施智平,关永,李勇坚,&魏洪兴.(2015).ROS中XML-RPC协议实现的形式化验证.小型微型计算机系统,36(12),2629-2633. |
| MLA | 贾娟娟,et al."ROS中XML-RPC协议实现的形式化验证".小型微型计算机系统 36.12(2015):2629-2633. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。