中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 软件所图书馆  > 期刊论文
Title:
ROS中XML-RPC协议实现的形式化验证
Alternative Title: Formal Verification of XML-RPC Protocol in ROS
Author: 贾娟娟 ; 施智平 ; 关永 ; 李勇坚 ; 魏洪兴
Keyword: ROS系统 ; XML-RPC协议 ; 有界模型检测 ; 定理证明
Source: 小型微型计算机系统
Issued Date: 2015
Volume: 36, Issue:12, Pages:2629-2633
Indexed Type: CSCD
Department: 贾娟娟, 首都师范大学信息工程学院, 高可靠嵌入式系统技术北京市工程研究中心;;电子系统可靠性技术北京市重点实验室, 北京 100048, 中国;施智平, 首都师范大学信息工程学院, 高可靠嵌入式系统技术北京市工程研究中心;;电子系统可靠性技术北京市重点实验室, 北京 100048, 中国;关永, 首都师范大学信息工程学院, 高可靠嵌入式系统技术北京市工程研究中心;;电子系统可靠性技术北京市重点实验室, 北京 100048, 中国;李勇坚, 中国科学院软件研究所, 计算机科学国家重点实验室, 北京 100080, 中国;魏洪兴, 北京航空航天大学机械工程及自动化学院, 北京 100191, 中国;
Abstract: XML-RPC协议是ROS节点通讯的核心调用机制,其实现的正确性关乎整个系统的顺利运行. 使用模型检测和定理证明结合的方法对ROS系统中的XML-RPC协议进行验证. 首先使用CBMC模型检测工具逐个验证协议源代码的函数,然后对模型检测不能全面验证的循环结构使用霍尔逻辑建立模型并在Isabelle /HOL定理证明器中验证. 本文的工作结合两种形式化方法的优点,既克服了定理证明人工干预过多、工作量繁杂的问题,又避免了模型检测中出现状态爆炸的问题.
English Abstract: 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.
Language: 中文
Citation statistics:
Content Type: 期刊论文
URI: http://ir.iscas.ac.cn/handle/311060/17384
Appears in Collections:软件所图书馆_期刊论文

Files in This Item:
File Name/ File Size Content Type Version Access License
ROS中XML-RPC协议实现的形式化验证.pdf(398KB)----限制开放 联系获取全文

Recommended Citation:
贾娟娟,施智平,关永,等. ROS中XML-RPC协议实现的形式化验证[J]. 小型微型计算机系统,2015-01-01,36(12):2629-2633.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[贾娟娟]'s Articles
[施智平]'s Articles
[关永]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[贾娟娟]‘s Articles
[施智平]‘s Articles
[关永]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2019  中国科学院软件研究所 - Feedback
Powered by CSpace