Test Generation with Inputs, Outputs, and Quiescence

ABSTRACT This paper studies testing based on labelled transition sys-tems, using the assumption that implementations communicate with their environment via inputs and outputs. Such implementations are formalized by restricting the class of transition systems to those systems that can al-ways accept input actions, as in input/output automata. Implementation relations, formalizing the notion of conformance of these implementations with respect to labelled transition system specications, are dened anal-ogous to the theory of testing equivalence and preorder. A test generation algorithm is given, which is proved to produce a sound and exhaustive test suite from a specication, i.e., a test suite that fully characterizes the set of correct implementations.