Original scientific paper

Exploring Properties of a Bounded Retransmission Protocol with VIS

Robert Meolic orcid.org/0000-0003-3395-1227 ; Faculty of Electrical Engineering and Computer Science, University of Maribor, Maribor, Slovenia
Tatjana Kapus ; Faculty of Electrical Engineering and Computer Science, University of Maribor, Maribor, Slovenia
Zmago Brezočnik orcid.org/0000-0003-4167-1882 ; Faculty of Electrical Engineering and Computer Science, University of Maribor, Maribor, Slovenia

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.

Keywords

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

Hrčak ID:

130484

URI

https://hrcak.srce.hr/130484

Publication date:

30.12.1999.

Visits: 736 *