TY - GEN
T1 - Quantitative verification of the bounded retransmission protocol
AU - Guo, Xu
AU - Xu, Ming
AU - Yang, Zongyuan
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84958544349
U2 - 10.1007/978-3-319-01766-2_141
DO - 10.1007/978-3-319-01766-2_141
M3 - 会议稿件
AN - SCOPUS:84958544349
SN - 9783319017655
T3 - Lecture Notes in Electrical Engineering
SP - 1245
EP - 1252
BT - Computer Engineering and Networking - Proceedings of the 2013 International Conference on Computer Engineering and Network, CENet 2013
PB - Springer Verlag
T2 - 3rd International Conference on Computer Engineering and Network, CENet 2013
Y2 - 20 July 2013 through 21 July 2013
ER -