RGMP-ROS混合机器人操作系统节点间通信的形式化验证

摘要 在机器人研发领域，通过将ROS机器人操作系统移植到Linux操作系统上可以解决工业机器人控制器软件模块化问题，但是，运行在Linux系统上的ROS不具有实时性，无法满足机器人运动的实时控制需求．RGMPROS是一个应用于工业机器人控制器的混合操作机器人系统，它能够解决ROS系统移植到Linux系统后的非实时性问题．因此，对RGMPROS混合操作系统的实时性验证有重要的意义．本文提出运用模型检测方法对RGMPROS系统节点间的通信进行验证．首先，对节点通信过程中的各部分建立时间自动机模型．然后用计算树逻辑公式对节点之间通信的可达性以及通信时间进行了形式化描述．最后在模型检测工具Uppaal中进行了验证．验证结果表明了RGMPROS系统具有实时性，可以满足实时性的需求