hrvatski

Formalna verifikacija komunikacijskih protokola u raspodijeljenim sustavima

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.

formalna verifikacija; provjera modela; vremenska logika; dijagrami binarnog odlučivanja; raspodijeljeni sustavi; protokoli

nije evidentirano