| | SLO | ENG | Piškotki in zasebnost

Večja pisava | Manjša pisava

Izpis gradiva

Naslov:Tvorjenje avtomatov linearnih končnih prič za formule ACTLW z orodjem EST
Avtorji:Vogrin, Rok (Avtor)
Kapus, Tatjana (Mentor) Več o mentorju... Novo okno
Meolic, Robert (Komentor)
Datoteke:.pdf MAG_Vogrin_Rok_2018.pdf (666,65 KB)
MD5: 376D00DBEEE8CB1376DE075ED1ED5D06
 
Jezik:Slovenski jezik
Vrsta gradiva:Magistrsko delo/naloga (mb22)
Tipologija:2.09 - Magistrsko delo
Organizacija:FERI - Fakulteta za elektrotehniko, računalništvo in informatiko
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
Leto izida:2018
Založnik:R. Vogrin
Izvor:[Maribor
UDK:004.8:621.395(043.2)
COBISS_ID:21776406 Novo okno
NUK URN:URN:SI:UM:DK:0WRUZOVQ
Število ogledov:464
Število prenosov:81
Metapodatki:XML RDF-CHPDL DC-XML DC-RDF
Področja:KTFMB - FERI
:
  
Skupna ocena:(0 glasov)
Vaša ocena:Ocenjevanje je dovoljeno samo prijavljenim uporabnikom.
Objavi na:AddThis
AddThis uporablja piškotke, za katere potrebujemo vaše privoljenje.
Uredi privoljenje...

Postavite miškin kazalec na naslov za izpis povzetka. Klik na naslov izpiše podrobnosti ali sproži prenos.

Licence

Licenca:CC BY-NC-ND 4.0, Creative Commons Priznanje avtorstva-Nekomercialno-Brez predelav 4.0 Mednarodna
Povezava:http://creativecommons.org/licenses/by-nc-nd/4.0/deed.sl
Opis:Najbolj omejujoča licenca Creative Commons. Uporabniki lahko prenesejo in delijo delo v nekomercialne namene in ga ne smejo uporabiti za nobene druge namene.
Začetek licenciranja:07.09.2018

Sekundarni jezik

Jezik:Angleški jezik
Naslov:Generating linear finite witness automata for ACTLW formulae with EST
Opis:This master's thesis deals with the generation of linear finite witness automata witnessing the validity of ACTLW (Action-based Computation Tree Logic with Unless operator) formulae in models of real systems called labelled transition systems. The purpose of this thesis is to generate witness automata showing how in such a model, properties described by a valid ACTLW formula are present. In the first part of the thesis, key notions for the generation of witness automata are defined. Characteristic functions and binary decision diagrams are introduced, as well as labelled transition systems, finite automata and the ACTLW logic. In the second part, a procedure for generating witness automata is described, along with its implementation with the EST toolbox. The generation of automata is demonstrated on a model of the bounded retransmission protocol and on a model of the lactose operon regulatory system.
Ključne besede:formal methods, model checking, temporal logic, witness automata, symbolic methods


Komentarji

Dodaj komentar

Za komentiranje se morate prijaviti.

Komentarji (0)
0 - 0 / 0
 
Ni komentarjev!

Nazaj
Logotipi partnerjev Univerza v Mariboru Univerza v Ljubljani Univerza na Primorskem Univerza v Novi Gorici