Protocol specification and validation using abstract data types and finite state machines

This thesis defines and develops a new method for the specification and validation of computer communication protocols. The method is based on the principles of abstract data types (ADTs), object oriented technology, and finite state machines (FSMs). The method, called SPASMs, which stands for Specification of Protocols with ADTs and FSMs, includes the definition of a protocol specification as a set of interconnected, independent but communicating modules. The modules use ADTs to represent the control information of the protocol while the FSM of the module provides the control of and interaction between the communicating ADTs. The SPASMs method is developed first by a introductory example, a simple Positive Acknowledgment with Retransmission Protocol (PAR). The specification method is developed in general terms, keeping the necessary finite machine character to assure that the technique will lead to a decidable protocol validation. The SPASMs technique is then shown to be capable of representing any finite protocol, as well as consistent with the application of protocol projection techniques to reduce global state space and protocol complexity.