Probabilistic Model Checking of Pipe protocol

Pipe protocol, proposed by Zhao [1] in early 2013, is one application layer protocol and one way to establish the Internet of Things, under which can different kinds of hardware platforms communicate with each other faster and more safely. As an upper layer protocol, Pipe protocol doesn't define details, but during the implementation, probabilistic and nondeterministic behaviors, such as data loss and external choice, are possible to happen. In this paper, we use probabilistic model checker, PRISM, to construct the probabilistic Pipe protocol as Probabilistic Timed Automata (PTAs), then verify some useful time-bounded properties, written in Probabilistic Computation Tree Logic (PCTL), like, "Maximum probability that the pipe is shut down after Source node sends all 5 data packets within 50 μs". The results show that the data loss probabilities, number of data and deadline should be restricted suitably if we require the maximum probability of the goal reaches some value. Our model is proved to be meaningful and we can give helpful suggestions to improve the implementation of Pipe protocol.