20.500.12556/DKUM-82146 Modeling, simulation, and verification of a Bounded Retransmission Protocol using Spin model checker and SpinRCP integrated development environment master's thesis Modeliranje, simulacija in preverjanje protokola z omejenim številom ponovnih oddaj z uporabo preverjalnika modelov Spin in integriranega razvojnega okolja SpinRCP Simple Promela Interpreter (Spin) is a model checker that uses Protocol Meta Language (PROMELA) to describe systems. Unfortunately, PROMELA does not support any time constructs, limiting the implementation of a Bounded Retransmission Protocol (BRP) in Spin's integrated development environment called Spin Rich Client Platform (SpinRCP). In the master's thesis, we model, simulate, and verify four versions of BRP. The first two versions are modeled without a timer, and with the others we show two different ways to simulate timers in PROMELA. The tests we run will show the time and space complexity of verifying each version depending on the size of the file sent and the number of retries to send each chunk. Simple Promela Interpreter (Spin) je preverjevalnik modelov, ki za opis sistemov uporablja jezik Protocol Meta Language (PROMELA). Na žalost PROMELA ne podpira nobenih časovnih konstruktov, kar omejuje implementacijo protokola z omejenim številom ponovnih oddaj (BRP) v integriranem razvojnem okolju za Spin, imenovanem Spin Rich Client Platform (SpinRCP). V magistrski nalogi modeliramo, simuliramo in verificiramo štiri različice BRP-ja. Prvi dve različici sta modelirani brez časovnika, z drugima pa prikazujemo dva različna načina za simulacijo časovnikov v jeziku PROMELA. Preizkusi, ki jih izvajamo, nam bodo pokazali časovno in prostorsko kompleksnost verifikacije vsake različice v odvisnosti od velikosti poslane datoteke in števila ponovnih poskusov oddaje posameznega kosa. model checker Bounded Retransmission Protocol Spin SpinRCP timer preverjanje modela protokol z omejenim številom ponovnih oddaj Spin SpinRCP časovnik true true false [P. Buden] Angleški jezik Slovenski jezik Magistrsko delo/naloga 2022-07-20 17:08:39 2022-10-20 14:43:24 2022-11-24 03:07:05 0000-00-00 00:00:00 2022 0 Maribor 0 Maribor 1 spletni vir (1 datoteka PDF (XXII, 144 f.)) 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 621.391(043.2) 130620419 MAG_Buden_Pero_2022.pdf MAG_Buden_Pero_2022.pdf 1 222C708E0B6AE517F20306B3B267175A 3ee822dc8d06ac95e82138f88d8a20dce70abec41576190390653e8f89f4164c 711808bb-1294-11ed-adc9-00155d000105 https://dk.um.si/Dokument.php?lang=slv&id=159700 Fakulteta za elektrotehniko, računalništvo in informatiko 0 0 0