运用定理证明器ACL2验证机器人操作系统ROS节点间通信

作     者：高雅 李晓娟 关永 王瑞 张杰 魏洪兴 GAO Ya;LI Xiao-juan;GUAN Yong;WANG Rui;ZHANG Jie;WEI Hong-xing

作者机构：高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性重点实验室首都师范大学信息工程学院北京100048 北京化工大学信息科学与技术学院北京100029 北京航空航天大学机械工程及自动化学院北京100191 

基　　金：国际科技合作计划项目(2011DFG13000)资助 北京市自然科学基金项目(4122017)资助 北京市教委科研基地建设项目(TJSHG201310028014)资助 国家自然科学基金项目(61373034 61303014)资助 

出 版 物：《小型微型计算机系统》 (Journal of Chinese Computer Systems)

年 卷 期：2014年第35卷第9期

页      码：2126-2130页

摘      要：作为一种开源的机器人操作系统,ROS在家用或服务性机器人上也得到广泛应用,保证其设计的正确性相当重要.本文通过定理证明的方法对ROS的节点间通信进行形式化建模与属性验证.对通信层的节点间连接建立和消息传递过程进行抽象建模,模型融合网络拓扑、主题匹配和路由机制等部分,定义函数对其进行描述,提取路由函数的存在性、可达性及正确性等3个关键属性,运用定理证明工具ACL2对ROS节点间通信的功能正确性进行自动验证,证明消息从源节点出发并选择有效的传输路径到达目的节点.这种满足属性要求的参数化模型具有一般性和易扩展性,并能保证ROS节点间通信的终止属性和功能正确性,可为ROS通信层设计的正确性验证工作提供一个有效的方法参考.

主 题 词：ROS ACL2 定理证明 参数化 自动验证 

学科分类：081203[081203] 08[工学] 0835[0835] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3969/j.issn.1000-1220.2014.09.037

馆 藏 号：203781902...