Executable logic specifications for protocol service interfaces

A general, formal modeling technique for protocol service interfaces is discussed. An executable description of the model using a logic-programming-based language, Prolog, is presented. The specification of protocol layers consists of two parts, the specification of the protocol interfaces and the specification of entities within the protocol layer. The specification of protocol interfaces forms the standard against which protocols are verified. When a protocol has been implemented, the correctness of its implementation can be tested using the sequences of events generated at the service interface. If the behavior of the protocol implementation is consistent with the behavior at the service interface, the implementation conforms to its standard. To illustrate how it works, the model is applied to the service interfaces of protocol standards developed for the transport layer of the ISO/OSI architecture. The results indicate that Prolog is a very useful formal language for specifying protocol interfaces