| 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...  |
|---|
| Files: |  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 |
|---|
| UDC: | 621.391(043.2) |
|---|
| COBISS.SI-ID: | 130620419 |
|---|
| Publication date in DKUM: | 20.10.2022 |
|---|
| Views: | 462 |
|---|
| Downloads: | 42 |
|---|
| Metadata: |    |
|---|
| Categories: | KTFMB - FERI
|
|---|
|
:
|
Copy citation |
|---|
| | | | Average score: | (0 votes) |
|---|
| Your score: | Voting is allowed only for logged in users. |
|---|
| Share: |  |
|---|
Hover the mouse pointer over a document title to show the abstract or click
on the title to get all document metadata. |
