Exploring Properties of a Bounded Retransmission Protocol with VIS

Robert Meolic, Tatjana Kapus, Zmago Brezočnik


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.


formal verification, bounded retransmission protocol, model checking, CTL, Verilog, VIS

Full Text:


Creative Commons License
This work is licensed under a Creative Commons Attribution-NoDerivatives 4.0 International License.

Crossref Similarity Check logo

Crossref logologo_doaj

 Hrvatski arhiv weba logo