Iskanje po katalogu digitalne knjižnice

Opis: Magistrsko delo zajema kratek opis konceptov in arhitekture programsko določenih omrežij. Sledita opis porazdeljene izvedbe krmilne ravnine in predstavitev glavnih pristopov zagotavljanja skladnosti v omrežjih s tako ravnino. Magistrsko delo se osredotoča na zagotavljanje skladnosti v omrežjih s krmilniki ONOS. Namen je predstavitev delovanja teh krmilnikov v grozdu in način zagotavljanja skladnosti njihovih informacij o topologiji omrežja. Delovanje grozda smo preizkusili v različnih scenarijih v navideznih omrežjih, tvorjenih z emulatorjem Mininet.
Ključne besede: programsko določeno omrežje, krmilnik, grozd, skladnost
Objavljeno: 30.11.2018; Ogledov: 414; Prenosov: 49
Celotno besedilo (2,78 MB)

Opis: Magistrsko delo obravnava tvorjenje avtomatov linearnih končnih prič veljavnosti formul akcijske logike dreves izvajanj z operatorjem unless (ACTLW -- Action-based Computation Tree Logic with Unless operator) v modelih realnih sistemov, imenovanih označeni sistemi prehajanja stanj. Namen dela je tvorjenje avtomatov prič, ki kažejo, kako so v takem modelu prisotne lastnosti, opisane z veljavno formulo ACTLW. V prvem delu naloge so predstavljeni ključni elementi za tvorjenje avtomatov prič. Vpeljana sta pojma karakteristična funkcija in binarni odločitveni graf. Definirani so označeni sistemi prehajanja stanj, končni avtomati ter logika ACTLW. V drugem delu je na podlagi definicij razvit postopek in opisana implementacija tvorjenja avtomatov linearnih končnih prič z orodjem EST. Tvorjenje avtomatov je prikazano na primeru modela komunikacijskega protokola z omejenim številom ponovnih oddaj in biološkega sistema uravnavanja laktoznega operona.
Ključne besede: formalne metode, preverjanje modelov, temporalna logika, avtomati prič, simbolične metode
Objavljeno: 09.10.2018; Ogledov: 465; Prenosov: 81
Celotno besedilo (666,65 KB)

Opis: V projektu smo se ukvarjali z avtomatizacijo analize povezav protokola TCP. Za analizo smo uporabili program tshark, ki je terminalska različica analizatorja protokolov Wireshark. Analiza je avtomatizirana s pomočjo skripta, napisanega v lupini Windows PowerShell. Za izvedbo projekta smo se podrobneje seznanili z delovanjem protokola TCP. V programskem delu je bilo treba spoznati tshark in principe pisanja skriptov v PowerShellu. Celoten razvoj skripta je potekal v razvojnem okolju Windows PowerShell ISE. V tem poročilu je najprej predstavljen problem, nato na kratko protokol TCP, Wireshark in PowerShell. Nazadnje je razložena celotna izvedba in delovanje našega skripta.
Ključne besede: protokol za nadzor prenosa, analiza omrežnega prometa, protokolni analizator, skript
Objavljeno: 26.01.2018; Ogledov: 919; Prenosov: 75
Celotno besedilo (1,40 MB)

Opis: Doktorska disertacija definira in raziskuje akcijsko logiko dreves izvajanj z operatorjem unless (ACTLW). ACTLW je izjavna temporalna logika razvejanega časa. Izhaja iz logike ACTL, ki je bila vpeljana leta 1990 in je ena od uveljavljenih temporalnih logik za izražanje lastnosti modelov, ki temeljijo na dogodkih. ACTLW je fleksibilnejša od ACTL, saj ne vsiljuje uporabe notranjega dogodka T pri izražanju lastnosti. ACTLW je tudi nekoliko izraznejša od ACTL, saj vsebuje temporalni operator unless (W), katerega pomena v ACTL ni možno v celoti izraziti. Nasprotno pa lahko vse formule ACTL izrazimo z uporabo operatorjev ACTLW. ACTLW omogoča učinkovito izvedbo preverjanja modelov s podobnimi algoritmi kot pri preverjanju modela s CTL, kar je pomembna izboljšava glede na logiko ACTL. Doktorska disertacija podaja definicijo logike ACTLW, izpeljave vseh standardnih temporalnih operatorjev in algoritme za globalno preverjanje modela z ACTLW s simboličnim računanjem. Predstavljeni so tudi algoritmi za tvorjenje diagnostike pri ACTLW, za tvorjenje lineamih prič in protiprimerov pri ACTLW ter za tvorjenje avtomatov prič in proti primerov pri ACTLW. Doktorska disertacija je v celoto zaokrožena z vzorci formul ACTLW in dvema večjima praktičnima primeroma: verifikacijo več različnih algoritmov za medsebojno izključevanje in verifikacijo dveh asinhronih vezij za porazdeljeno medsebojno izključevanje.
Ključne besede: formalne metode verifikacije sistemov, preverjanje modela, temporalna logika, doktorske disertacije, CTL, ACTL, ACTLW, diagnostika, problem medsebojnega izključevanja
Objavljeno: 04.08.2017; Ogledov: 723; Prenosov: 71
Celotno besedilo (1,04 MB)

Opis: This paper concerns the formal modelling of medium access control in nonbeacon-enabled IEEE 802.15.4 wireless personal area networks with probabilistic timed automata supported by the PRISM probabilistic model checker. In these networks, the devices contend for the medium by executing an unslotted carrier sense multiple access with collision avoidance algorithm. In the literature, a model of a network which consists of two stations sending data to two different destination stations is introduced. We have improved this model and, based on it, we propose two ways of modelling a network with an arbitrary number of sending stations, each having its own destination. We show that the same models are valid representations of a star-shaped network with an arbitrary number of stations which send data to the same destination station. We also propose how to model such a network if some of the sending stations are not within radio range of the others, i.e. if they are hidden. We present some results obtained for these models by probabilistic model checking using PRISM.
Ključne besede: wireless personal area network, medium access control, hidden station, formal specification, probabilistic model checking
Objavljeno: 15.06.2017; Ogledov: 526; Prenosov: 254
Celotno besedilo (2,25 MB)
Gradivo ima več datotek! Več...