magistrsko delo
Robert Meolic (Author), Tatjana Kapus (Mentor), Zmago Brezočnik (Co-mentor)

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;

Data

Language: Slovenian
Year of publishing:
Typology: 2.09 - Master's Thesis
Organization: UM FERI - Faculty of Electrical Engineering and Computer Science
Publisher: [R. Meolic]
UDC: 621.39:681.326.77
COBISS: 4972822 Link will open in a new window
Views: 1903
Downloads: 71
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: Checking correctness of concurrent systems behaviour
Secondary abstract: This master thesis is about methods for checking corectness of concurrent systems behaviour based on the system specification with a process algebra. A definition of the process algebra and some examples of system specifications in terms of process are given. The master thesis presents the checking of trace equivalence, and symbolic model checking with propositional branching-time temporal logic ACTL. All discussed methods together form an efficient tool for formal verification of systems. An implementation of such atool with BDDs is described. The usage of the tool is demonstrated on the verification of communication protocol BRP.
Secondary keywords: formal methods of system verification;concurrent systems;process algebra;observational equivalences;testing equivalences;symbolic model checking;ACTL;BDD;
URN: URN:SI:UM:
Type (COBISS): Master's thesis
Thesis comment: Mag. delo, Univ. Maribor, Fakulteta za elektrotehniko, računalništvo in informatiko, 1999
Pages: XXII, 208 str.
ID: 10852666