magistrsko delo
Rok Vogrin (Author), Tatjana Kapus (Mentor), Robert Meolic (Co-mentor)

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

Data

Language: Slovenian
Year of publishing:
Typology: 2.09 - Master's Thesis
Organization: UM FERI - Faculty of Electrical Engineering and Computer Science
Publisher: R. Vogrin
UDC: 004.8:621.395(043.2)
COBISS: 21776406 Link will open in a new window
Views: 778
Downloads: 113
Average score: 0 (0 votes)
Metadata: JSON JSON-RDF JSON-LD TURTLE N-TRIPLES XML RDFA MICRODATA DC-XML DC-RDF RDF

Other data

Secondary language: English
Secondary title: Generating linear finite witness automata for ACTLW formulae with EST
Secondary abstract: 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.
Secondary keywords: formal methods;model checking;temporal logic;witness automata;symbolic methods;
URN: URN:SI:UM:
Type (COBISS): Master's thesis/paper
Thesis comment: Univ. v Mariboru, Fak. za elektrotehniko, računalništvo in informatiko, Telekomunikacije
Pages: VII, 81 str.
ID: 10958016