magistrsko delo
Rok Vogrin (Avtor), Tatjana Kapus (Mentor), Robert Meolic (Komentor)

Povzetek

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;magistrske naloge;

Podatki

Jezik: Slovenski jezik
Leto izida:
Tipologija: 2.09 - Magistrsko delo
Organizacija: UM FERI - Fakulteta za elektrotehniko, računalništvo in informatiko
Založnik: R. Vogrin
UDK: 004.8:621.395(043.2)
COBISS: 21776406 Povezava se bo odprla v novem oknu
Št. ogledov: 778
Št. prenosov: 113
Ocena: 0 (0 glasov)
Metapodatki: JSON JSON-RDF JSON-LD TURTLE N-TRIPLES XML RDFA MICRODATA DC-XML DC-RDF RDF

Ostali podatki

Sekundarni jezik: Angleški jezik
Sekundarni naslov: Generating linear finite witness automata for ACTLW formulae with EST
Sekundarni povzetek: 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.
Sekundarne ključne besede: formal methods;model checking;temporal logic;witness automata;symbolic methods;
URN: URN:SI:UM:
Vrsta dela (COBISS): Magistrsko delo/naloga
Komentar na gradivo: Univ. v Mariboru, Fak. za elektrotehniko, računalništvo in informatiko, Telekomunikacije
Strani: VII, 81 str.
ID: 10958016