This thesis presents a protocol specification, a validation and a verification methods.
Protocol specification and verification technique presented here is similar to that of Sabnani. Protocol is a set of interacting components. In his method, each component is separately specified, FSM(finite state machine) for safety properties, temporal logic for liveness properties, and he use Buchi automata in the process of verification. But, his method check only some of deadlocks. In order to guarantee that the verification method is complete, some extensive validation method is needed to check completely deadlocks and indefinite postponements.
In this thesis, the specification is done by BFSM, semantics of which is slightly extended from that of Buchi automata so that both safety and liveness properties are specified in BFSM. And, validation method implied by given definitions and theorems check completely not only deadlocks and indefinite postponements, but also livelocks. So, this guarantee that given verification method is complete.
