A Framework for Interoperability Testing of Network Protocols

In this report, we extend the testing theory based on formal specifications by formalizing testing for interoperability with a new relation intop. Intuitively, P intop_{S} 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 labelled transition systems. Existing notions of implementation preorders and equivalences 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).