| | SLO | ENG | Piškotki in zasebnost

Večja pisava | Manjša pisava
Prva stran > Izpis gradiva

Izpis gradiva Pomoč

Naslov:Modeling, simulation, and verification of a Bounded Retransmission Protocol using Spin model checker and SpinRCP integrated development environment : master's thesis
Avtorji:ID Buden, Pero (Avtor)
ID Brezočnik, Zmago (Mentor) Več o mentorju... Novo okno
Datoteke:.pdf MAG_Buden_Pero_2022.pdf (3,54 MB)
MD5: 222C708E0B6AE517F20306B3B267175A
 
Jezik:Angleški jezik
Vrsta gradiva:Magistrsko delo/naloga
Tipologija:2.09 - Magistrsko delo
Organizacija:FERI - Fakulteta za elektrotehniko, računalništvo in informatiko
Opis: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.
Ključne besede:model checker, Bounded Retransmission Protocol, Spin, SpinRCP, timer
Kraj izida:Maribor
Kraj izvedbe:Maribor
Založnik:[P. Buden]
Leto izida:2022
Št. strani:1 spletni vir (1 datoteka PDF (XXII, 144 f.))
PID:20.500.12556/DKUM-82146 Novo okno
UDK:621.391(043.2)
COBISS.SI-ID:130620419 Novo okno
Datum objave v DKUM:20.10.2022
Število ogledov:462
Število prenosov:42
Metapodatki:XML DC-XML DC-RDF
Področja: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 [na spletu]. Magistrsko delo. Maribor : P. Buden. [Dostopano 9 april 2025]. Pridobljeno s: https://dk.um.si/IzpisGradiva.php?lang=slv&id=82146
Kopiraj citat
  
Skupna ocena:
0.5
1
1.5
2
2.5
3
3.5
4
4.5
5
(0 glasov)
Vaša ocena:Ocenjevanje je dovoljeno samo prijavljenim uporabnikom.
Objavi na:Bookmark and Share


Postavite miškin kazalec na naslov za izpis povzetka. Klik na naslov izpiše podrobnosti ali sproži prenos.

Licence

Licenca:CC BY-NC-ND 4.0, Creative Commons Priznanje avtorstva-Nekomercialno-Brez predelav 4.0 Mednarodna
Povezava:http://creativecommons.org/licenses/by-nc-nd/4.0/deed.sl
Opis:Najbolj omejujoča licenca Creative Commons. Uporabniki lahko prenesejo in delijo delo v nekomercialne namene in ga ne smejo uporabiti za nobene druge namene.
Začetek licenciranja:20.07.2022

Sekundarni jezik

Jezik:Slovenski jezik
Naslov:Modeliranje, simulacija in preverjanje protokola z omejenim številom ponovnih oddaj z uporabo preverjalnika modelov Spin in integriranega razvojnega okolja SpinRCP
Opis: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.
Ključne besede:preverjanje modela, protokol z omejenim številom ponovnih oddaj, Spin, SpinRCP, časovnik


Komentarji

Dodaj komentar

Za komentiranje se morate prijaviti.

Komentarji (0)
0 - 0 / 0
 
Ni komentarjev!

Nazaj
Logotipi partnerjev Univerza v Mariboru Univerza v Ljubljani Univerza na Primorskem Univerza v Novi Gorici