20.500.12556/DKUM-67092 Preverjanje pravilnosti obnašanja sistemov s sočasnostjo magistrsko delo Checking correctness of concurrent systems behaviour 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. 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. formalne metode verifikacije sistemi s sočasnostjo procesne algebre opazovalne ekvivalence testne ekvivalence simbolično preverjanje modelov ACTL BDD formal methods of system verification concurrent systems process algebra observational equivalences testing equivalences symbolic model checking ACTL BDD true true false Slovenski jezik Angleški jezik Delo ni kategorizirano 2017-08-02 11:48:06 2017-08-04 08:46:49 2022-08-01 13:32:19 2019-07-11 16:08:45 0 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 621.39:681.326.77 4972822 URN:SI:UM:DK:CUJAZD3E magister.pdf magister.pdf 1 D2E2E50DB1C58FD72FC3F896F9E74556 ca7f1f9cb3c85d823d9d0fc08bd43848a5fb40d3f40162fa771b96dccfcffdd1 7653a983-7c0e-11eb-bb7a-00155d0001ca 20.500.12556/dkum/ecc8ed70-2024-4a38-aa29-ed5e56801083 https://dk.um.si/Dokument.php?lang=slv&id=114700 Fakulteta za elektrotehniko, računalništvo in informatiko 0 0 0