主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公English
2022年专刊出版计划 微信服务介绍 最新一期:2021年第2期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
芦倩,李晓娟,关永,王瑞,施智平.面向数据流的ROS2数据分发服务形式建模与分析.软件学报,2021,32(6):26-0
面向数据流的ROS2数据分发服务形式建模与分析
Modeling and Analysis of ROS2 Data Distribution Service for Data Flow
投稿时间:2020-08-30  修订日期:2020-10-26
DOI:10.13328/j.cnki.jos.006251
中文关键词:  ROS2  数据分发服务  QoS  概率时间自动机  PRISM  形式化建模与分析
英文关键词:ROS2  data distribution service  QoS  probabilistic timed automata  PRISM  formal modeling and analysis
基金项目:国家重点研发计划(2019YFB1309900);国家自然科学基金(61876111);科技创新服务能力建设(00620530290073)首都师范大学交叉科学研究项目(19530012005)
作者单位E-mail
芦倩 首都师范大学 信息工程学院, 北京 100048
高可靠嵌入式系统北京市工程研究中心(首都师范大学), 北京 100048 
 
李晓娟 首都师范大学 信息工程学院, 北京 100048
高可靠嵌入式系统北京市工程研究中心(首都师范大学), 北京 100048 
lixj@cnu.edu.cn 
关永 首都师范大学 信息工程学院, 北京 100048
北京成像理论与技术高精尖创新中心(首都师范大学), 北京 100048 
 
王瑞 首都师范大学 信息工程学院, 北京 100048
轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 100048 
 
施智平 首都师范大学 信息工程学院, 北京 100048
轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 100048 
 
摘要点击次数: 122
全文下载次数: 35
中文摘要:
      机器人操作系统(Robot Operating System,简称ROS)是一种开源的元操作系统,能够在异种计算簇上提供基于消息机制的结构化通信层,为改善ROS1中存在的数据分发实时性、可靠性问题,ROS2提出了面向数据流的数据分发服务机制,本文采用概率模型检验的方法,分析、验证ROS2系统数据分发机制的实时性和可靠性,首先提出了一种面向数据流的ROS2数据分发服务的形式化验证框架,并对通信系统模块建立概率时间自动机模型;其次,运用概率模型检测器,通过数据丢失率和系统响应时间等参数分析、验证ROS2面向数据流的数据分发服务的实时性、可靠性.最后基于重传机制、服务质量(Quality of Service,简称QoS)策略分析,通过设置和调整服务质量参数,实现不同的数据需求和传输方式的量化性能分析,为ROS2应用的设计人员以及基于数据流的分布式数据分发服务的形式化建模、验证和量化性能分析提供参考.
英文摘要:
      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 proposed data flow oriented data distribution service mechanism, this article adopts the method of probability model test and analysis, validate ROS2 system real-time performance and reliability of the data distribution mechanism, first put forward a data flow oriented ROS2 formal validation framework of data distribution service and for communication system module and probabilistic timed automata model is set up; Secondly, the probability model detector is used to analyze and verify the real-time performance and reliability of ROS2 data stream-oriented data distribution service through parameters such as data loss rate and system response time. Finally based on retransmission mechanism, Quality of Service (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, for ROS2 application designers and distributed data distribution Service based on the data flow of formal modeling, validation, and quantitative performance analysis to provide the reference.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利