Exploring Properties of a Bounded Retransmission Protocol with VIS

Abstract

It is of great interest for users of communication protocols to have a proof that they are correct and reliable to use. In order to prove a protocol correct formally, the protocol and the required properties must be form ally described. This paper reports on verifying properties of a bounded retransmission protocol for large data packets. It is used to transfer files via a lossy communication channel. We emphasize timing properties of the protocol. We specified the protocol in Verilog and stated properties in a computation tree logic. The verification was carried out automatically by model checking. We used the non-commercial tool VIS which made it possible to introduce nondeterministic choice of data packets length and a realistic notion of time.