In order to verify the reliability of the bounded retransmission protocol, probabilistic model checking technology is used in this paper. The integer semantics approach is introduced, which allows working directly at the level of the original probabilistic timed automaton (PTA). In such a method, clocks are viewed as counters storing nonnegative integer values, which increase as time passes. The PTA modeling the system can then be seen as a discrete-time Markov chain. Based on this fact, the protocol is modeled directly with DTMC. Properties are described in probabilistic computation tree logic. By making an analysis of the quantitative properties of the protocol, a threshold is obtained. Experimental result shows that no matter how many chunks to be transmitted, if the maximum retransmitted time is greater than or equal to 3, the protocol can be considered reliable. Method in this paper can not only verify the correctness of a system but also make analysis of nonfunctional indices of a system such as reliability or performance.
展开▼
