| 本文已被：浏览 3287次 下载 7128次 |
码上扫一扫！ |
|
|
| 面向数据流的ROS2数据分发服务形式建模与分析 |
|
芦倩1,2, 李晓娟1,2, 关永1,3, 王瑞1,4, 施智平1,4
|
|
1.首都师范大学 信息工程学院, 北京 100048;2.高可靠嵌入式系统技术北京市工程研究中心(首都师范大学), 北京 100048;3.北京成像理论与技术高精尖创新中心(首都师范大学), 北京 100048;4.轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 100048
|
|
| 摘要: |
| 机器人操作系统（robot operating system，简称ROS）是一种开源的元操作系统，能够在异种计算簇上提供基于消息机制的结构化通信层.为改善ROS1中存在的数据分发实时性、可靠性问题，ROS2提出了面向数据流的数据分发服务机制.采用概率模型检验的方法，分析、验证ROS2系统数据分发机制的实时性和可靠性.首先，提出一种面向数据流的ROS2数据分发服务的形式化验证框架，并对通信系统模块建立概率时间自动机模型；其次，运用概率模型检测器，通过数据丢失率和系统响应时间等参数分析、验证ROS2面向数据流的数据分发服务的实时性、可靠性；最后，基于重传机制、服务质量（quality of service，简称QoS）策略分析，通过设置和调整服务质量参数，实现不同的数据需求和传输方式的量化性能分析，为ROS2应用的设计人员以及基于数据流的分布式数据分发服务的形式化建模、验证和量化性能分析提供参考. |
| 关键词: ROS2 数据分发服务 QoS 概率时间自动机 PRISM 形式化建模与分析 |
| DOI：10.13328/j.cnki.jos.006251 |
| 分类号: |
| 基金项目:国家重点研发计划（2019YFB1309900）；国家自然科学基金（61876111）；科技创新服务能力建设-基本科研业务费（00620530290073）；首都师范大学交叉科学研究项目（0062155087） |
|
| Modeling and Analysis of ROS2 Data Distribution Service for Data Flow |
|
LU Qian1,2, LI Xiao-Juan1,2, GUAN Yong1,3, WANG Rui1,4, SHI Zhi-Ping1,4
|
|
1.College of Information Engineering, Capital Normal University, Beijing 100048, China;2.Beijing Engineering Research Center of High Reliable Embedded System (Capital Normal University), Beijing 100048, China;3.Beijing Advanced Innovation Center for Imaging Theory and Technology (Capital Normal University), Beijing 100048, China;4.Beijing Key Laboratory of Light Industrial Robot and Safety Verification (Capital Normal University), Beijing 100048, China
|
| Abstract: |
| Robot operating system (ROS) is an open source meta-operating system, which can provide a structured communication layer based on message mechanism on heterogeneous computing clusters. In order to improve the real-time and reliability problems of data distribution in ROS1, ROS2 is proposed with data flow oriented data distribution service mechanism. This study adopts the method of probability model test and analysis, validates real-time and reliability of the ROS2 system. Firstly, a data flow oriented ROS2 data distribution service system of communication formal validation framework is put forward, and the communication system module probabilistic timed automata model is set up. Secondly, probabilistic model detector PRISM is used to verify the real-time and reliability of ROS2 data flow oriented data distribution service through parameter analysis of data loss rate and system response time. Finally, based on retransmission mechanism, quality of service (QoS) strategy analysis, through the set up and adjust service quality parameters, different data requirements and quantitative performance analysis of transmission mode are achieved, providing the reference for application designers based on ROS2 and distributed data distribution service based on the data flow of formal modeling, validation, and quantitative performance analysis. |
| Key words: ROS2 data distribution service QoS probabilistic timed automata PRISM formal modeling and analysis |
