Abstract:Robot Operating System (ROS) is an open-source, meta-operating system, which can provide a structured communication layer based on the message mechanism on heterogeneous computing clusters. To improve the unsatisfactory real-time performance and reliability of data distribution in ROS1, ROS2 is proposed with a data flow-oriented data distribution service mechanism. This study validates the real-time performance and reliability of the ROS2 data distribution mechanism by means of probabilistic model checking. Firstly, a formal validation framework is put forward for the data flow-oriented ROS2 data distribution service system, and the probabilistic timed automata model is set up for the communication system module. Secondly, the probabilistic model checker PRISM is used to verify the real-time performance and reliability of data flow-oriented ROS2 data distribution service through the analysis of data loss rate and system response time. Finally, depending on the retransmission mechanism and Quality of Service (QoS) policy analysis, different data requirements and quantitative performance analysis of the transmission mode are achieved through the setting and adjustment of QoS parameters. This study can provide references for ROS2 application designers and the formal modeling, validation, and quantitative performance analysis of the distributed data distribution service based on the data flow.