Preverjanje pravilnosti obnašanja sistemov s sočasnostjoMeolic, Robert (Avtor) Kapus, Tatjana (Mentor) Brezočnik, Zmago (Komentor) formalne metode verifikacijesistemi s sočasnostjoprocesne algebreopazovalne ekvivalencetestne ekvivalencesimbolično preverjanje modelovACTLBDDMagistrsko 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.02017-08-02 11:48:06Delo ni kategorizirano67092UDK: 621.39:681.326.77COBISS_ID: 4972822NUK URN: URN:SI:UM:DK:CUJAZD3Esl