Most approaches to model based testing, or testing from a formal specification, represent testing as a process that involves synchronous communication between the tester and a model representing the system under test (SUT). However, many real systems interact with their environment (or a tester) through asynchronous channels: we have asynchronous testing. The asynchronous nature of communications may result from there being a network between the SUT and the tester. However, it might also result from the use of a test tool in which an adapter buffers outputs received from the SUT until they can be processed. Naturally, we can see asynchronous testing as being the synchronous testing of the composition of the model N of the SUT with a model of the communications channel. While this is a general solution, the model of the communications channel has an infinite number of states if the channel is unbounded; even if the channel is bounded the number of states is exponential in this bound.
An alternative, to introducing a model of the communications channel, is to take into account the asynchronous nature of communications when reasoning about testing and generating test cases. When interacting asynchronously with the SUT, the observation of output from the SUT is delayed and input supplied by the tester is received later by the SUT. Thus, a trace (sequence of inputs and outputs) observed by the tester might not be a trace of the SUT. For example, if the tester sends input ?i twice and then observes output !o (trace ?i?i!o) then it is quite possible that output !o was produced by the SUT before any input was received or in response to the first input. Things are even worse when the communications channel is not first-in-first-out (FIFO) since inputs sent by the tester might be received in a different order and outputs produced by the SUT might also be reordered.
If we wish to adapt our testing framework for use in asynchronous testing then we need to change several things. First, we need a different notion of what it means for an observed trace to be allowed by a state machine model (specification) M. This corresponds to a different notion of what it means for one state machine N (the unknown model representing the SUT) to conform to another state machine M (the specification). This is explored in the first of the papers below, with corresponding implementation relations (for FIFO and non-FIFO) being defined. While conformance is decidable for synchronous testing (given finite state machines N and M), it transpires that it is generally undecidable for asynchronous testing (both FIFO and non-FIFO). This also means that it is generally undecidable whether there is a test case that can distinguish a model N (representing a possible behaviour of the SUT) from a specification M, and also whether there is a test case that can distinguish two states. In addition, if we have a property represented by a finite automaton P then it is also undecidable whether any observation that might be made when interacting asynchronously with a model M is in the language defined by P (this is a form of model checking). However, the paper gives some conditions under which these problems are decidable.
A second issue we might consider is whether we can generate test cases, or parts of test cases, that are guaranteed to achieve certain objectives (given a finite state model M). The second paper below considers this for three objectives: reaching a given state s of M, executing a given transition t of M, and distinguishing two states s and s' of M. For FIFO communications and finite state M (that does not have a state from which it is possible to take an infinite walk that has only internal transitions and outputs), we have the following results: these problems can be solved in polynomial time as long as M is observable but otherwise are EXPTIME-complete. For non-FIFO channels the results are worse: all three test generation problems are EXPTIME-hard even for deterministic models and the oracle problem, of deciding whether an observation is allowed by a model M, is NP-complete.
Back to Rob Hierons' home page
Last updated: October 2012.