Max-Plus Matrix Method for Correctness Verification of Communication Protocols ?

摘要

Accompanied with the mushroom growth of communication technology, the correct operation of protocols has been widely concerned and studied in the field of communication. The correctness verification is a difficult problem due to the state space explosion. In this paper, the event graph model of a communication protocol is established and the verification matrix is proposed to verify the correctness of the protocol. It is found out that the correctness of a protocol is equivalent to the nilpotency of the verification matrix on the max-plus algebra framework. The matrix method is constructive and leads to a polynomial algorithm for verifying the correctness of protocols. Some examples about stop-and-wait protocols and handshake protocols are taken to illustrate how the presented results work in practical applications.