A fresh look at testing for asynchronous communication

Testing is one of the fundamental techniques for verifying if a computing system conforms to its specification. We take a fresh look at the theory of testing for message-passing systems based on a natural notion of observability in terms of input-output relations. We propose two notions of test equivalence: one which corresponds to presenting all test inputs up front and the other which corresponds to interactively feeding inputs to the system under test. We compare our notions with those studied earlier, notably the equivalence proposed by Tretmans. In Tretmans’ framework, asynchrony is modelled using synchronous communication by augmenting the state space of the system with queues. We show that the first equivalence we consider is strictly weaker than Tretmans’ equivalence and undecidable, whereas the second notion is incomparable. We also establish (un)decidability results for these equivalences