论文部分内容阅读
在机器人研发领域,通过将ROS机器人操作系统移植到Linux操作系统上可以解决工业机器人控制器软件模块化问题,但是,运行在Linux系统上的ROS不具有实时性,无法满足机器人运动的实时控制需求.RGMP-ROS是一个应用于工业机器人控制器的混合操作机器人系统,它能够解决ROS系统移植到Linux系统后的非实时性问题.因此,对RGMP-ROS混合操作系统的实时性验证有重要的意义.本文提出运用模型检测方法对RGMP-ROS系统节点间的通信进行验证.首先,对节点通信过程中的各部分建立时间自动机模型.然后用计算树逻辑公式对节点之间通信的可达性以及通信时间进行了形式化描述.最后在模型检测工具Uppaal中进行了验证.验证结果表明了RGMP-ROS系统具有实时性,可以满足实时性的需求.
In the field of robotics development, the problem of modularization of industrial robot controller software can be solved by porting the ROS robot operating system to the Linux operating system. However, the ROS running on Linux systems are not real-time and can not meet the real-time control needs of robot motion .RGMP-ROS is a hybrid robotic system for industrial robot controllers that solves the non-real-time nature of a ROS system after being ported to a Linux system.Therefore, it is important to verify the real-time performance of the RGMP-ROS hybrid operating system Significance.This paper proposes the use of model detection method to verify the communication between RGMP-ROS system nodes.Firstly, a time automaton model is established for each part of the node communication process.And then using the tree logic formula to reach the communication between the nodes Sex and communication time were formally described.Finally, the model verification tool Uppaal was used to verify the results.Experimental results show that the RGMP-ROS system is real-time and can meet the real-time requirements.