hrcak mascot   Srce   HID

Journal of computing and information technology, Vol.7 No.4 December 1999.

Original scientific paper

Exploring Properties of a Bounded Retransmission Protocol with VIS

Robert Meolic   ORCID icon 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 icon orcid.org/0000-0003-4167-1882 ; Faculty of Electrical Engineering and Computer Science, University of Maribor, Maribor, Slovenia

Fulltext: english, pdf (5 MB) pages 311-321 downloads: 142* cite
APA 6th Edition
Meolic, R., Kapus, T. & Brezočnik, Z. (1999). Exploring Properties of a Bounded Retransmission Protocol with VIS. Journal of computing and information technology, 7 (4), 311-321. Retrieved from https://hrcak.srce.hr/130484
MLA 8th Edition
Meolic, Robert, et al. "Exploring Properties of a Bounded Retransmission Protocol with VIS." Journal of computing and information technology, vol. 7, no. 4, 1999, pp. 311-321. https://hrcak.srce.hr/130484. Accessed 23 Oct. 2018.
Chicago 17th Edition
Meolic, Robert, Tatjana Kapus and Zmago Brezočnik. "Exploring Properties of a Bounded Retransmission Protocol with VIS." Journal of computing and information technology 7, no. 4 (1999): 311-321. https://hrcak.srce.hr/130484
Harvard
Meolic, R., Kapus, T., and Brezočnik, Z. (1999). 'Exploring Properties of a Bounded Retransmission Protocol with VIS', Journal of computing and information technology, 7(4), pp. 311-321. Available at: https://hrcak.srce.hr/130484 (Accessed 23 October 2018)
Vancouver
Meolic R, Kapus T, Brezočnik Z. Exploring Properties of a Bounded Retransmission Protocol with VIS. Journal of computing and information technology [Internet]. 1999 Dec 30 [cited 2018 October 23];7(4):311-321. Available from: https://hrcak.srce.hr/130484
IEEE
R. Meolic, T. Kapus and Z. Brezočnik, "Exploring Properties of a Bounded Retransmission Protocol with VIS", Journal of computing and information technology, vol.7, no. 4, pp. 311-321, december 1999. [Online]. Available: https://hrcak.srce.hr/130484. [Accessed: 23 October 2018]

Abstracts
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

Visits: 199 *