Formal Verification of Communication Protocols in Distributed Systems

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 onda 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.Protocols represent a crucial part of distributed computer systems. Main characteristics of the distributed systems is a concurrent nonterminating execution. Reasoning about such systems is difficult because of the obvious lack of an intuition. Distributed systems are gaining widespread usage in many safety critical applications. Development of such systems is usually based on informal procedures based on a textual description or a graphical representation. In another words, the design is almost completely based on an intuition. The errors caused by such way of development are then being detected and corrected using an informal techniques. It is obvious that this approach will not increase the confidence in correctness of the systems being developed. In this work formal verification of the protocols in distributed systems is presented. Methodology that have been used for the verification is based on an analysis of the finite state systems. Concrete technique that has been used is called symbolic model checking,and it is based on the manipulation of the binary decision diagrams. Tools that have enabled automatic verification are called SMV and NuSMV. This work shows the three examples of the formal verification. Each example demonstrates how different model checking methods can be used in formal analysis of the protocols in distributed systems