Iskanje po katalogu digitalne knjižnice

Opis: In an article published in IEEE Access in 2020, researchers present an approach to using TLA + for the formal verification of whether a network of SDN (Software-Defined Networking) switches implements the filtering rules of a given monolithic firewall. The distributed as well as monolithic firewalls are specified with TLA + . It is shown that the correctness of the former with respect to the latter can be verified automatically by using the TLC model checker. The main contributions of this paper are the following improvements of that approach. Firstly, by specifying switches without using any variables, the time needed for the model checking is reduced significantly. For example, the verification of the same networks takes a few seconds with the new approach and does not end after several hours with the previous one. Secondly, the following problem is solved. With the latter, if a monolithic firewall allows a packet to pass through, all the paths in the distributed firewall which the packet is routed on must allow the same. Otherwise, the model checker proclaims the distributed firewall to be in error. We present an additional approach to the verification, which gives a positive answer if at least one of the paths allows the packet to pass through.
Ključne besede: firewalls, formal specification, formal verification, logic, model checking, software defined networking
Objavljeno v DKUM: 04.12.2023; Ogledov: 285; Prenosov: 30
Celotno besedilo (1,24 MB)
Gradivo ima več datotek! Več...

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 v DKUM: 30.11.2018; Ogledov: 1202; Prenosov: 123
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 v DKUM: 09.10.2018; Ogledov: 1477; Prenosov: 164
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 v DKUM: 26.01.2018; Ogledov: 1979; Prenosov: 101
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 v DKUM: 04.08.2017; Ogledov: 1995; Prenosov: 126
Celotno besedilo (1,04 MB)