微信服务号

微信订阅号

2025年4月3日 7:45 星期四
首页 > 过刊浏览>2021年第32卷第6期 >1818-1829. DOI:10.13328/j.cnki.jos.006251
PDF HTML阅读 XML下载 导出引用 引用提醒
面向数据流的ROS2数据分发服务形式建模与分析
作者:
作者简介:

芦倩(1993-),女,硕士,主要研究领域为嵌入式系统形式建模与验证,网络协议分析.
王瑞(1981-),女,博士,教授,博士生导师,主要研究领域为形式化方法,软件安全验证.
李晓娟(1968-),女,博士,教授,博士生导师,主要研究领域为嵌入式系统形式建模与验证,网络协议分析.
施智平(1974-),男,博士,教授,博士生导师,主要研究领域为形式化方法,人工智能.
关永(1966-),男,博士,教授,博士生导师,主要研究领域为形式化验证,高可靠嵌入式系统,机器人.

通讯作者:

李晓娟，lixj@cnu.edu.cn

基金项目:

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


Modeling and Analysis of ROS2 Data Distribution Service for Data Flow
Author:
Fund Project:

National key Research and development program (2019YFB1309900); National Natural Science Foundation of China (61876111); Capacity Building for Sci-Tech Innovation-Fundamental Scientific Research Funds (00620530290073); Research Fund from Academy for Multidisciplinary Studies of Capital Normal University (0062155087)

  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [21]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

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

    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.

    参考文献
    [1] Jiang Z, Gong Y, Zhai J, et al. Message passing optimization in robot operating system. Int'l Journal of Parallel Programming, 2019,48(1):119-136.
    [2] Pardo-Castellote G, Farabaugh B, Warren R. An introduction to DDS and data-centric communications. RTI, 2005.
    [3] García-Valls M, Domínguez-Poblete J, Touahria IE. Using DDS middleware in distributed partitioned systems. ACM SIGBED Review, 2018,14(4):14-20.
    [4] Dong W, Wang J, Qi ZC. Model checking for concurrent and real-time systems. Computer Research and Development, 2001, 38(6):698-705(in Chinese with English abstract).
    [5] He F, Baresi L, Ghezzi C, et al. Formal analysis of publish-subscribe systems by probabilistic timed automata. In:Proc. of the Int'l Conf. on Formal Techniques for Networked and Distributed Systems. Berlin, Heidelberg:Springer, 2007. 247-262.
    [6] Liu Y, Guan Y, Li X, et al. Formal analysis and verification of DDS in ROS2. In:Proc. of the 201816th ACM/IEEE Int'l Conf. on Formal Methods and Models for System Design (MEMOCODE). IEEE, 2018. 1-5.
    [7] Yin J, Zhu H, Fei Y, et al. Formalization and verification of RTPS StatefulWriter module using CSP. In:Proc. of the 31st Int'l Conf. on Software Engineering and Knowledge Engineering. 2019.
    [8] Maruyama Y, Kato S, Azumi T. Exploring the performance of ROS2. In:Proc. of the 13th Int'l Conf. on Embedded Software. ACM, 2016. 5.
    [9] Inglés-Romero JF, Romero-Garcés A, Vicente-Chicote C, et al. A model-driven approach to enable adaptive QoS in DDS-based middleware. IEEE Trans. on Emerging Topics in Computational Intelligence, 2017,1(3):176-187.
    [10] Casini D, Blaß T, Lütkebohle I, et al. Response-Time analysis of ROS 2 processing chains under reservation-based scheduling. In:Proc. of the 31st Euromicro Conf. on Real-Time Systems (ECRTS 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019.
    [11] Kim J, Smereka JM, Cheung C, et al. Security and performance considerations in ROS 2:A balancing act. 2018.
    [12] Schlesselman JM, Pardo-Castellote G, Farabaugh B. OMG data-distribution service (DDS):Architectural update. In:Proc. of the IEEE MILCOM 2004 Military Communications Conf. IEEE, 2004. 961-967.
    [13] Guesmi T, Rekik R, Hasnaoui S, et al. Design and performance of DDS-based middleware for real-time control systems. IJCSNS, 2007,7(12):188-200.
    [14] Corsaro A, Schmidt DC. The data distribution service-The communication middleware fabric for scalable and extensible systems-of-systems. System of Systems, 2012.
    [15] Chen C. Design and implementation of data distribution system based on DDS[Master. Thesis]. Shamghai:Fudan University, 2008(in Chinese with English abstract).
    [16] Norman G, Parker D, Sproston J. Model checking for probabilistic timed automata. Formal Methods in System Design, 2013,43(2):164-190.
    [17] Kwiatkowska M, Norman G, Parker D. PRISM:Probabilistic symbolic model checker. In:Proc. of the Int'l Conf. on Modelling Techniques and Tools for Computer Performance Evaluation. Berlin, Heidelberg:Springer, 2002. 200-204.
    [18] Kwiatkowska M, Norman G, Parker D. PRISM:Probabilistic model checking for performance and reliability analysis. ACM SIGMETRICS Performance Evaluation Review, 2009,36(4):40-45.
    附中文参考文献:
    [4] 董威,王戟,齐治昌.并发和实时系统的模型检验技术.计算机研究与发展,2001,38(6):698-705.
    [15] 陈春甫.基于DDS的数据分发系统的设计与实现[硕士学位论文].上海:复旦大学,2008.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

芦倩,李晓娟,关永,王瑞,施智平.面向数据流的ROS2数据分发服务形式建模与分析.软件学报,2021,32(6):1818-1829

复制
分享
文章指标
  • 点击次数:2376
  • 下载次数: 5751
  • HTML阅读次数: 3270
  • 引用次数: 0
历史
  • 收稿日期:2020-08-30
  • 最后修改日期:2020-10-26
  • 在线发布日期: 2021-02-07
  • 出版日期: 2021-06-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19778341位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号