软件学报

作者：芦倩，李晓娟，关永，王瑞，施智平

单位：芦倩，首都师范大学 信息工程学院, 北京 100048;高可靠嵌入式系统技术北京市工程研究中心(首都师范大学), 北京 10004811,李晓娟，首都师范大学 信息工程学院, 北京 100048;高可靠嵌入式系统技术北京市工程研究中心(首都师范大学), 北京 10004802,关永，首都师范大学 信息工程学院, 北京 100048;北京成像理论与技术高精尖创新中心(首都师范大学), 北京 10004803,王瑞，首都师范大学 信息工程学院, 北京 100048;轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 10004804,施智平，首都师范大学 信息工程学院, 北京 100048;轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 10004805

关键词：ROS2;数据分发服务;QoS;概率时间自动机;PRISM;形式化建模与分析

基金：国家重点研发计划（2019YFB1309900）；国家自然科学基金（61876111）；科技创新服务能力建设-基本科研业务费（00620530290073）；首都师范大学交叉科学研究项目（0062155087）

机器人操作系统（robot operating system，简称ROS）是一种开源的元操作系统，能够在异种计算簇上提供基于消息机制的结构化通信层.为改善ROS1中存在的数据分发实时性、可靠性问题，ROS2提出了面向数据流的数据分发服务机制.采用概率模型检验的方法，分析、验证ROS2系统数据分发机制的实时性和可靠性.首先，提出一种面向数据流的ROS2数据分发服务的形式化验证框架，并对通信系统模块建立概率时间自动机模型；其次，运用概率模型检测器，通过数据丢失率和系统响应时间等参数分析、验证ROS2面向数据流的数据分发服务的实时性、可靠性；最后，基于重传机制、服务质量（quality of service，简称QoS）策略分析，通过设置和调整服务质量参数，实现不同的数据需求和传输方式的量化性能分析，为ROS2应用的设计人员以及基于数据流的分布式数据分发服务的形式化建模、验证和量化性能分析提供参考.

来源：2021年第6期

《软件学报》期刊编辑部

查看软件学报杂志2021年第6期