| | SLO | ENG | Piškotki in zasebnost

Večja pisava | Manjša pisava

Iskanje po katalogu digitalne knjižnice Pomoč

Iskalni niz: išči po
išči po
išči po
išči po
* po starem in bolonjskem študiju

Opcije:
  Ponastavi


1 - 2 / 2
Na začetekNa prejšnjo stran1Na naslednjo stranNa konec
1.
Modeling, simulation, and verification of a Bounded Retransmission Protocol using Spin model checker and SpinRCP integrated development environment : master's thesis
Pero Buden, 2022, magistrsko delo

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
Objavljeno v DKUM: 20.10.2022; Ogledov: 462; Prenosov: 39
.pdf Celotno besedilo (3,54 MB)

2.
Applying automated model extraction for simulation and verification of real-life SDL specification with spin
Boštjan Vlaovič, Aleksander Vreže, Zmago Brezočnik, 2017, izvirni znanstveni članek

Opis: Formally defined Specification and Description Language (SDL) is used for the design and specification of complex safety-critical systems. Each change in the specification of the product should be immediately checked formally against the requirements’ specification. This paper presents semi-automated system abstraction, automated model extraction, simulation, and formal verification of real-life complex SDL specification. Sound algorithms implemented in our sdl2pml automated model extraction tool preserve all properties of the SDL system. Sdl2pml includes our model of discrete time, abstraction, and support for all relevant SDL functionality and constructs such as dynamic process creation, rational data types, and communication with more than one process instance. To the best of our knowledge, most of them are not supported by any other known approach. We use our SpinRCP tool for simulation and formal verification of the extracted model with the Spin model checker. We demonstrate the applicability of our approach on ISDN User adaptation protocol from SI3000 Softswitch. The extracted Promela model is the largest one ever processed by Spin. We have shown that Spin simulation and model checking can be applied successfully to such huge models.
Ključne besede: formal specifications, automated extraction, formal languages, simulation, formal verification, model cheking, SDL, Promela, SpinRCP, Sdl2pml
Objavljeno v DKUM: 03.08.2017; Ogledov: 1402; Prenosov: 429
.pdf Celotno besedilo (13,46 MB)
Gradivo ima več datotek! Več...

Iskanje izvedeno v 0.07 sek.
Na vrh
Logotipi partnerjev Univerza v Mariboru Univerza v Ljubljani Univerza na Primorskem Univerza v Novi Gorici