Pregled bibliografske jedinice broj: 232305
Formalna verifikacija komunikacijskih protokola u raspodijeljenim sustavima
Formalna verifikacija komunikacijskih protokola u raspodijeljenim sustavima, 2005., magistarski rad, Fakultet elektrotehnike i računarstva, Zagreb
CROSBI ID: 232305 Za ispravke kontaktirajte CROSBI podršku putem web obrasca
Naslov
Formalna verifikacija komunikacijskih protokola u raspodijeljenim sustavima
(Formal verification of communication protocols in distributed systems)
Autori
Pek, Edgar
Vrsta, podvrsta i kategorija rada
Ocjenski radovi, magistarski rad
Fakultet
Fakultet elektrotehnike i računarstva
Mjesto
Zagreb
Datum
03.11
Godina
2005
Stranica
150
Mentor
Bogunović, Nikola
Neposredni voditelj
Bogunović, Nikola
Ključne riječi
formalna verifikacija; provjera modela; vremenska logika; dijagrami binarnog odlučivanja; raspodijeljeni sustavi; protokoli
(formal verification; model checking; temporal logic; binary decision diagrams; distributed systems; protocols)
Sažetak
Protokoli predstavljaju ključni dio raspodijeljenih računalnih sustava. Osnovna karakteristika raspodijeljenih sustava je konkurentno neterminirajuće izvršavanje. Rasuđivanje o takvim sustavima je teško već zbog očitog nedostatka intuitivne slike. Raspodijeljeni računalni sustavi sve više postaju sastavni dio mnogih sustava čije je ispravno funkcioniranje iznimno važno. Pri tome se razvoj takvih sustava obično zasniva na neformalnim postupcima baziranim na tekstualnom opisu ili na korištenju grafičkih prikaza. Drugim riječima, razvoj se gotovo potpuno zasniva na intuiciji. Takav način vrlo često dovodi do mnogih grešaka koje se nastoje detektirati i ispraviti korištenjem neformalnim tehnika. Očito takav pristup neće povečati povjerenje u ispravnost sustava koji se razvija. U ovom radu pokazana je formalna verifikacija protokola u raspodijeljenim sustavima. Metodologija koja je korištena prilikom verifikacije temelji se na analizi konačnih modela. Konkretno, korištena je simbolička provjera modela bazirana na manipulaciji dijagrama binarnog odlučivanja. Alati koji su omogućili automatsku verifikaciju nazivaju se SMV i NuSMV. Rad pokazuje tri primjera formalne verifikacije. Pomoću svakog primjera nastoji se pokazati kako razne metode provjere modela mogu koristiti u analizi protokola u raspodijeljenim računalnim sustavima.
Izvorni jezik
Hrvatski
Znanstvena područja
Računarstvo
