Conformance Checking of Components Against Their Non-deterministic 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 implementation. 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 component that manages all of the angelic non-determinism for an arbitrary 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-deterministic specifications of components and their low-level implementations in sync.