论文部分内容阅读
作为一种开源的机器人操作系统,ROS在家用或服务性机器人上也得到广泛应用,保证其设计的正确性相当重要.本文通过定理证明的方法对ROS的节点间通信进行形式化建模与属性验证.对通信层的节点间连接建立和消息传递过程进行抽象建模,模型融合网络拓扑、主题匹配和路由机制等部分,定义函数对其进行描述,提取路由函数的存在性、可达性及正确性等3个关键属性,运用定理证明工具ACL2对ROS节点间通信的功能正确性进行自动验证,证明消息从源节点出发并选择有效的传输路径到达目的节点.这种满足属性要求的参数化模型具有一般性和易扩展性,并能保证ROS节点间通信的终止属性和功能正确性,可为ROS通信层设计的正确性验证工作提供一个有效的方法参考.
As an open-source robotic operating system, ROS is widely used in home or service robots to ensure the correctness of the design.This paper formally models and attributes ROS inter-node communication by theorem-proven methods Verification.An abstract modeling of node-by-node connection establishment and message passing in the communication layer is carried out.The model merges the network topology, theme matching and routing mechanism and so on, defines the function to describe it, extracts the existence, reachability of the routing function and Correctness and other three key attributes, the use of theorem proving tool ACL2 ROS inter-node communication function of the correctness of the automatic verification that the message departure from the source node and select a valid transmission path to the destination node.This parameter to meet the property requirements The model has generality and expansibility, and can guarantee the termination attribute and function correctness of communication between ROS nodes, which can provide an effective method reference for the correctness verification of ROS communication layer design.