Formal modelling and analysis of TCP for nodes communication with ROS

Abstract

TCP (transportation control protocol) is widely used for supporting communications between robotic nodes with ROS (robotic operation system) for critical-task implementation. The probability of bit errors and lost packets is much higher for moving nodes under WLAN. So it is essential to analyze the performance and the reliability of the communication processes for nodes with ROS. It is built that the communication model of nodes for TCP in ROS by MDP(Markov Decision Process) and the reliability of that is analyzed in this paper. The Specifications of the TCP for nodes communication is formalized into the objective properties by PCTL(Probabilistic Computation Tree Logic), and the satisfiability of the properties is verified by the probabilistic model checker. The results can help the designers to make better strategies for the communication process over TCP in ROS of robotic nodes.