Conformance checking of components against their nondeterministic specifications

Conformance checking of a component is a testing method to see if an implementation and its executable specification are behaviorally equivalent relative to any interactions performed on the implementa-tion. Such checking is complicated by the presence of non-determinism in the specification: the specification may permit a set of possible behaviors. We present a new method to automatically derive a com-ponent that manages all of the angelic non-determinism for an ar-bitrary implementation/specification pair. The new component just plugs in; no instrumentation of any implementation is necessary. Conformance checking thus helps to keep high-level non-determinstic specifications of components and their low-level implementations in sync