FORMAL VERIFICATION OF COMMUNICATION PROTOCOLS IN DISTRIBUTED SYSTEMS

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 
ifinite  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.

Keywords: formal verification, model checking, temporal logic, binary decision diagrams, 
distributed systems,
protocols