A framework for interoperability testing of network protocols

The authors extend the testing theory based on formal specifications by formalizing testing for interoperability with a new relation, intop. Intuitively, P intop Q if, for every event offered by either P or Q, the concurrent execution of P and Q will be able to proceed with the traces in S, where S is their (common) specification. This theory is applicable to formal description methods that allow a semantic interpretation of specifications in terms of labeled transition systems. Some existing notions of implementation relations in protocol testing theory are placed in this framework and their discriminating power for identifying processes which will interoperate is examined. As an example, a subset of the ST-II protocol is formally specified and its possible implementations are shown to interoperate if each implementation satisfies the intop relation with respect to S, the specification of the ST-II protocol (subset)