| | SLO | ENG | Cookies and privacy

Bigger font | Smaller font

Search the digital library catalog Help

Query: search in
search in
search in
search in
* old and bologna study programme

Options:
  Reset


1 - 10 / 26
First pagePrevious page123Next pageLast page
1.
Tvorjenje avtomatov linearnih končnih prič za formule ACTLW z orodjem EST
Rok Vogrin, 2018, master's thesis

Abstract: 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.
Keywords: formalne metode, preverjanje modelov, temporalna logika, avtomati prič, simbolične metode
Published: 09.10.2018; Views: 489; Downloads: 81
.pdf Full text (666,65 KB)

2.
Representation of Boolean functions with ROBDDs
Aleš Časar, Robert Meolic, independent scientific component part or a chapter in a monograph

Abstract: This paper describes data structures and algorithms for representation of Boolean functions with reduced ordered binary decision diagrams (ROBDDs). A hash table is used for quick search. Additional information about variables and functions is stored in binary trees. Manipulations on functions are based on a recursive algorithm of ITE operation. The primary goal of this article is describe programming technics needed to realize the idea. For the first time here recursive algorithms for composing functions and garbage collection with a formulae counter are presented. This is better than garbage collection in other known implementations. The results of the tests show that the described representation is very efficient in applications which operate with Boolean functions.
Keywords: Reduced Ordered Binary Decision Diagram, Boolean function, logic functions, logic design verification, hash table
Published: 02.02.2018; Views: 1380; Downloads: 32
.pdf Full text (323,32 KB)

3.
Implementation aspects of a BDD package supporting general decision diagrams
Robert Meolic, 2016, invited lecture at foreign university

Abstract: General decision diagram is a loose term for a superset of different types of decision diagrams - we are interested in joining BDDs, FDDs, and different types of suppressed DDs, e.g. ZBDDs. I will present: The current state of our BDD package Biddy (functionalities and details about the original implementation aspects). Our ideas for efficient implementation of ZBDDs (which could be used for all types of suppressed DDs).New type od decision diagrams called ZFDD (somehow symmetric to ZBDD). A rough draft about the implementation of a package supporting general decision diagrams.
Keywords: Binary Decision Diagram, Zero-suppressed Binary Decision Diagram, Boolean function, Algorithm, BDD package, Biddy
Published: 26.10.2017; Views: 1549; Downloads: 58
.pdf Full text (1,07 MB)

4.
Uporaba urejenih odločitvenih grafov pri računalniški obdelavi logičnih funkcij
Robert Meolic, 1995, undergraduate thesis

Abstract: Odločitveni grafi so uspešna podatkovna struktura za predstavitev logičnih funkcij. V diplomskem delu so podane potrebne matematične osnove za njihovo razumevanje in računalniški algoritmi za njihovo učinkovito realizacijo. Podrobno so opisani urejeni binarni odločitveni grafi (OBDD), urejeni funkcijski odločitveni grafi (OFDD) in urejeni binarni odločitveni grafi s potlačenimi ničlami (0-sup-BDD). Dodan je pregledni opis prostih binarnih odločitvenih grafov (FBDD), razširjenih binarnih odločitvenih grafov (XBDD), urejenih Kroneckerjevih funkcijskih odločitvenih grafov (OKFDD) in diferenčnih binarnih odločitvenih grafov (\delta BDD). Za ROBDD, ROFDD in 0-sup-BDD so podani razčlenitveno pravilo, pravilo minimizacije in algoritmi za logične operacije, ki so tudi izpeljani. Algoritmi so bili realizirani v programskem jeziku C. Prikazani so rezultati testov, v katerih se primerja učinkovitost različnih vrst odločitvenih grafov pri preverjanju enakosti logičnih funkcij, pri predstavitvi množic kombinacij in pri predstavitvi slik.
Keywords: Boolova algebra, logične funkcije, binarni odločitveni grafi, funkcijski odločitveni grafi, podatkovne strukture
Published: 07.08.2017; Views: 1344; Downloads: 90
.pdf Full text (560,59 KB)

5.
Akcijska logika dreves izvajanj z operatorjem unless
Robert Meolic, doctoral dissertation

Abstract: 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.
Keywords: formalne metode verifikacije sistemov, preverjanje modela, temporalna logika, doktorske disertacije, CTL, ACTL, ACTLW, diagnostika, problem medsebojnega izključevanja
Published: 04.08.2017; Views: 766; Downloads: 71
.pdf Full text (1,04 MB)

6.
Preverjanje pravilnosti obnašanja sistemov s sočasnostjo
Robert Meolic, master's thesis

Abstract: Magistrsko delo obravnava metode preverjanja pravilnosti obnašanja sistemov, ki temeljijo na opisu sistema s procesno algebro. Podana je definicija procesne algebre in primeri opisov sistemov s procesi. Predstavljeno je ugotavljanje ekvivalence sledi, stroge, vejitvene in šibke opazovalne ekvivalence, ugotavljanje testne ekvivalence ter simbolično preverjanje modelov z izjavno vejitveno temporalno logiko ACTL. Vse obravnavane metode se med seboj odlično dopolnjujejo in skupaj tvorijo močno orodje za formalno verifikacijo sistemov. V magistrskem delu je opisana izvedba takšnega orodja z BDD-ji. Uporaba orodja je ponazorjena na primeru verifikacije komunikacijskega protokola BRP.
Keywords: formalne metode verifikacije, sistemi s sočasnostjo, procesne algebre, opazovalne ekvivalence, testne ekvivalence, simbolično preverjanje modelov, ACTL, BDD
Published: 04.08.2017; Views: 1541; Downloads: 59
.pdf Full text (1,10 MB)

7.
Universal decomposition rule for OBDD, OFDD, and 0-sup-BDD
Robert Meolic, Zmago Brezočnik, 2016

Abstract: Binary decision diagram (BDD) is a very successful data structure for representation and manipulation of Boolean functions. Various BDD types have been proposed. In this paper relations between OBDD, OFDD, and 0-sup-BDD are shown in a new way. An universal decomposition rule for them is introduced. Using this rule a set of 288 BDD types is defined together with their minimization rules. NOTE: This is a revisited and translated version of the paper: "Splošno razčlenitveno pravilo za OBDD, OFDD in 0-sup-BDD". In Proceedings of the Fifth Electrotechnical and Computer Science Conference ERK'96, Portorož, Slovenia, volume B, pages 11-14, September 1996.
Keywords: Binary Decision Diagram, Shannon's expansion, Reed–Muller expansion, Davio expansion, Digital Circuit Design
Published: 12.10.2016; Views: 1133; Downloads: 67
.pdf Full text (235,92 KB)

8.
ANALIZA PODATKOV LOKALNEGA BREZŽIČNEGA OMREŽJA S POMOČJO SNMP
Cveto Ljubič, 2016, undergraduate thesis

Abstract: V diplomskem delu Analiza podatkov lokalnega brezžičnega omrežja s pomočjo SNMP smo opisali nekaj lastnosti brezžičnih omrežij in delovanje standarda IEEE 802.11. Preučili smo razvoj protokola SNMP in naredili primerjavo med različicami. Za uspešno izvedbo testnega modela smo prilagodili računalnik in strežnik za delo s storitvijo SNMP in programskim jezikom PHP in po potrebi prilagodili tudi obstoječe brezžično omrežje. Naredili smo zajem podatkov gostov s pomočjo protokola SNMP in uporabne podatke shranili v bazo podatkov. Nad shranjenimi podatki smo naredili analizo in preučili, kako bazo podatkov in prihod strank povežemo v lojalnostni program z dodano vrednostjo. Preučili smo določila zakonodaje v primeru posredovanja podatkov v komercialne namene, pridobljenih od gostov. Raziskavo smo najprej opravili na testnem omrežju in ne v lokalu. Pri opisu zakonodaje smo se omejili samo na nekatere vidike. Končali smo z analizo izsledkov teoretične raziskave, kakor tudi praktične aplikacije.
Keywords: brezžično omrežje, Wi-Fi, SNMP, lojalnostni program, PHP, zakonodaja
Published: 13.09.2016; Views: 782; Downloads: 68
.pdf Full text (1,55 MB)

9.
RAZVOJ INFORMACIJSKEGA SISTEMA ZA SPREMLJANJE IGRE NA IGRALNIH AVTOMATIH
Bojan Pehan, 2016, undergraduate thesis

Abstract: V diplomskem delu smo predstavili izdelavo lastnega informacijskega sistema za spremljanje igre na igralnih avtomatih (ISIA), ki je združljiv z že obstoječim sistemom v ostalih Hitovih igralnicah in skupaj s sistemom proizvajalca Bally tvori popoln sistem sledenja igralcev. Da lahko spremljamo igro na igralnem avtomatu, potrebujemo napravo, s katero lahko zajemamo spremenljivke igralnega avtomata. Za ta namen smo razvili svojo strojno in programsko opremo. Vzporedno smo razvili še aplikacijo, ki je namenjena za upravljanje s sistemom. Po uspešnem testiranju smo v igralnici vzpostavili celotno mrežno infrastrukturo, ki je temelj za nemoteno delovanje sistema. Po izvedbi omrežja smo začeli z montažo pripadajoče opreme na posamezne igralne avtomate in sistem je bil pripravljen za uporabo. V nalogi smo še predstavili igralne avtomate in njihovo delovanje ter nadzorno informacijski sistem igralnih avtomatov.
Keywords: sledenje gostov, igralni avtomati, casino, stikala
Published: 01.08.2016; Views: 1392; Downloads: 180
.pdf Full text (3,50 MB)

10.
IZVAJANJE POSKUSOV S PROGRAMSKO DEFINIRANIMI OMREŽJI Z EMULATORJEM MININET
Danijel Ovčar, 2016, undergraduate thesis

Abstract: V diplomskem delu je predstavljena tehnologija programsko definiranih omrežij ter funkcionalnost in uporaba programskega okolja Mininet. Mininet nam omogoča tvorjenje virtualnih omrežij na enem računalniku. Je koristna programska oprema, ki se uporablja za raziskovanje, testiranje in odpravo napak, ki se lahko pojavijo v dejanskem omrežju. Predstavljena je namestitev programskega okolja Mininet na operacijski sistem Windows. S pomočjo orodja Mininet smo izvajali različne poskuse na programsko definiranih omrežjih, zasnovanih z uporabo programskega jezika python. Pri delu smo se omejili na uporabo stikal OpenFlow in krmilnikov POX ter predstavili njihovo delovanje.
Keywords: programsko definirana omrežja, stikala, OpenFlow, emulacija omrežij, python
Published: 11.04.2016; Views: 843; Downloads: 88
.pdf Full text (3,52 MB)

Search done in 0.3 sec.
Back to top
Logos of partners University of Maribor University of Ljubljana University of Primorska University of Nova Gorica