| | SLO | ENG | Cookies and privacy

Bigger font | Smaller font
First page > Show document

Show document Help

Title:Modeling, simulation, and verification of a Bounded Retransmission Protocol using Spin model checker and SpinRCP integrated development environment : master's thesis
Authors:ID Buden, Pero (Author)
ID Brezočnik, Zmago (Mentor) More about this mentor... New window
Files:.pdf MAG_Buden_Pero_2022.pdf (3,54 MB)
MD5: 222C708E0B6AE517F20306B3B267175A
 
Language:English
Work type:Master's thesis/paper
Typology:2.09 - Master's Thesis
Organization:FERI - Faculty of Electrical Engineering and Computer Science
Abstract: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.
Keywords:model checker, Bounded Retransmission Protocol, Spin, SpinRCP, timer
Place of publishing:Maribor
Place of performance:Maribor
Publisher:[P. Buden]
Year of publishing:2022
Number of pages:1 spletni vir (1 datoteka PDF (XXII, 144 f.))
PID:20.500.12556/DKUM-82146 New window
UDC:621.391(043.2)
COBISS.SI-ID:130620419 New window
Publication date in DKUM:20.10.2022
Views:462
Downloads:42
Metadata:XML DC-XML DC-RDF
Categories:KTFMB - FERI
:
BUDEN, Pero, 2022, Modeling, simulation, and verification of a Bounded Retransmission Protocol using Spin model checker and SpinRCP integrated development environment : master’s thesis [online]. Master’s thesis. Maribor : P. Buden. [Accessed 25 April 2025]. Retrieved from: https://dk.um.si/IzpisGradiva.php?lang=eng&id=82146
Copy citation
  
Average score:
0.5
1
1.5
2
2.5
3
3.5
4
4.5
5
(0 votes)
Your score:Voting is allowed only for logged in users.
Share:Bookmark and Share


Searching for similar works...Please wait....

Similar works from other repositories:
  1. Link between child sexual abuse and suicidal behavior
Hover the mouse pointer over a document title to show the abstract or click on the title to get all document metadata.

Licences

License:CC BY-NC-ND 4.0, Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
Link:http://creativecommons.org/licenses/by-nc-nd/4.0/
Description:The most restrictive Creative Commons license. This only allows people to download and share the work for no commercial gain and for no other purposes.
Licensing start date:20.07.2022

Secondary language

Language:Slovenian
Title:Modeliranje, simulacija in preverjanje protokola z omejenim številom ponovnih oddaj z uporabo preverjalnika modelov Spin in integriranega razvojnega okolja SpinRCP
Abstract: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.
Keywords:preverjanje modela, protokol z omejenim številom ponovnih oddaj, Spin, SpinRCP, časovnik


Comments

Leave comment

You must log in to leave a comment.

Comments (0)
0 - 0 / 0
 
There are no comments!

Back
Logos of partners University of Maribor University of Ljubljana University of Primorska University of Nova Gorica