Implementation Relations for Testing Through Asynchronous Channels

This paper concerns testing from an input-output transition system (IOTS) model of a system under test that interacts with its environment through asynchronous first in first out (FIFO) channels. It explores methods for analysing an IOTS without modelling the channels. If IOTS M produces sequence sigma, then, since communications are asynchronous, output can be delayed and so a different sequence might be observed. Thus, M defines a language Tr(M) of sequences that can be observed when interacting with M through FIFO channels. We define implementation relations and equivalences in terms of Tr(M): an implementation relation says how IOTS N must relate to IOTS M in order for N to be a correct implementation of M. It is important to use an appropriate implementation relation since otherwise the verdict from a test run might be incorrect and also because it influences test generation. It transpires that it is undecidable whether IOTS N conforms to IOTS M and so also whether there is a test case that can distinguish between two IOTSs. We also investigate the situation in which we have a finite automaton P and either wish to know whether Tr(M) boolean AND L(P) is empty or whether Tr(M) boolean AND Tr(P) is empty and prove that these are undecidable. In addition, we give conditions under which conformance and intersection are decidable.