hrcak mascot   Srce   HID

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

Izvorni znanstveni članak

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

Puni tekst: engleski, pdf (5 MB) str. 311-321 preuzimanja: 138* citiraj
APA 6th Edition
Meolic, R., Kapus, T. i Brezočnik, Z. (1999). Exploring Properties of a Bounded Retransmission Protocol with VIS. Journal of computing and information technology, 7 (4), 311-321. Preuzeto s 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, br. 4, 1999, str. 311-321. https://hrcak.srce.hr/130484. Citirano 19.08.2018.
Chicago 17th Edition
Meolic, Robert, Tatjana Kapus i Zmago Brezočnik. "Exploring Properties of a Bounded Retransmission Protocol with VIS." Journal of computing and information technology 7, br. 4 (1999): 311-321. https://hrcak.srce.hr/130484
Harvard
Meolic, R., Kapus, T., i Brezočnik, Z. (1999). 'Exploring Properties of a Bounded Retransmission Protocol with VIS', Journal of computing and information technology, 7(4), str. 311-321. Preuzeto s: https://hrcak.srce.hr/130484 (Datum pristupa: 19.08.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]. 30.12.1999. [pristupljeno 19.08.2018.];7(4):311-321. Dostupno na: https://hrcak.srce.hr/130484
IEEE
R. Meolic, T. Kapus i Z. Brezočnik, "Exploring Properties of a Bounded Retransmission Protocol with VIS", Journal of computing and information technology, vol.7, br. 4, str. 311-321, Kolovoz 2018. [Online]. Dostupno na: https://hrcak.srce.hr/130484. [Citirano: 19.08.2018.]

Sažetak
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.

Ključne riječi
formal verification; bounded retransmission protocol; model checking; CTL; Verilog; VIS

Hrčak ID: 130484

URI
https://hrcak.srce.hr/130484

Posjeta: 193 *