Testing Labelled Transition Systems with Inputs and Outputs

摘要

This paper studies testing based on labelled transition systems, using theassumption that implementations communicate with their environment via inputs and outputs. A testing theory for these implementations is developed, analogous to the theory of testing equivalence and preorder. The theory consists of implementation relations formalizing conformance of these implementations with respect to labelled transition system specifications, test cases and test suites, test execution, the notion of passing a test suite, and a test generation algorithm, which is proved to produce sound test suites for one of the implementation relations.