| | SLO | ENG | Cookies and privacy

Bigger font | Smaller font

Show document

Title:Preverjanje pravilnosti obnašanja sistemov s sočasnostjo : magistrsko delo
Authors:Meolic, Robert (Author)
Kapus, Tatjana (Mentor) More about this mentor... New window
Brezočnik, Zmago (Co-mentor)
Files:.pdf magister.pdf (1,10 MB)
 
Language:Slovenian
Work type:Not categorized (r6)
Typology:2.09 - Master's Thesis
Organization:FERI - Faculty of Electrical Engineering and Computer Science
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
UDC:621.39:681.326.77
COBISS_ID:4972822 Link is opened in a new window
NUK URN:URN:SI:UM:DK:CUJAZD3E
License:CC BY 4.0
This work is available under this license: Creative Commons Attribution 4.0 International
Views:308
Downloads:34
Metadata:XML RDF-CHPDL DC-XML DC-RDF
Categories:Misc.
:
  
Average score:(0 votes)
Your score:Voting is allowed only for logged in users.
Share:AddThis
AddThis uses cookies that require your consent. Edit consent...

Hover the mouse pointer over a document title to show the abstract or click on the title to get all document metadata.

Secondary language

Language:English
Title:Checking correctness of concurrent systems behaviour
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.
Keywords:formal methods of system verification, concurrent systems, process algebra, observational equivalences, testing equivalences, symbolic model checking, ACTL, BDD


Comments

Leave comment

You have to log in to leave a comment.

Comments (0)
0 - 0 / 0
 
There are no comments!

Back
Logos of partners University of Maribor University of Ljubljana University of Primorska University of Nova Gorica