Paper Info
Title
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.
Year
DOI
Venue
2016
10.1007/978-3-319-59288-6_61
Lecture Notes of the Institute for Computer Sciences, Social Informatics, and Telecommunications Engineering
Keywords
Field
DocType
Node network communication,Probabilistic model checking,Markov decision process
Computer science,Satisfiability,Network packet,Computer network,Markov decision process,Probabilistic CTL,Models of communication,Statistical model,Probabilistic model checking,Bit error rate,Distributed computing
Conference
Volume
ISSN
Citations 
201
1867-8211
0
PageRank 
References 
Authors
0.34
0
5
Name
Order
Citations
PageRank
Xiaojuan Li1144.14
Yanyan Huo200.34
Yong Guan378782.67
Rui Wang402.03
Jie Zhang5366.46