  We present a new approach to conformance testing of black-box reactive
systems. We consider system specifications written as linear temporal logic
formulas to generate tests as sequences of input/output pairs: inputs are
extracted from the Buchi automata corresponding to the specifications, and
outputs are obtained by feeding the inputs to the systems. Conformance is
checked by comparing input/output sequences with automata traces to detect
violations of the specifications. We consider several criteria for extracting
tests and for stopping generation, and we compare them experimentally using
both indicators of coverage and error-detection. The results show that our
methodology can generate test suites with good system coverage and
error-detection capability.
