magistrsko delo
Robert Meolic (Avtor), Tatjana Kapus (Mentor), Zmago Brezočnik (Komentor)

Povzetek

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.

Ključne besede

formalne metode verifikacije;sistemi s sočasnostjo;procesne algebre;opazovalne ekvivalence;testne ekvivalence;simbolično preverjanje modelov;ACTL;BDD;

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. Meolic]
UDK: 621.39:681.326.77
COBISS: 4972822 Povezava se bo odprla v novem oknu
Št. ogledov: 1903
Št. prenosov: 71
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: Checking correctness of concurrent systems behaviour
Sekundarni povzetek: 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.
Sekundarne ključne besede: formal methods of system verification;concurrent systems;process algebra;observational equivalences;testing equivalences;symbolic model checking;ACTL;BDD;
URN: URN:SI:UM:
Vrsta dela (COBISS): Magistrsko delo
Komentar na gradivo: Mag. delo, Univ. Maribor, Fakulteta za elektrotehniko, računalništvo in informatiko, 1999
Strani: XXII, 208 str.
ID: 10852666