Unifying Input Output Conformance

2nd International Symposium on Unifying Theories of Programming (delegate proceedings), pages 97 – 116.

Model-based conformance testing aims to assess the correct- ness of an implementation with respect to a specification. This raises the question of a proper conformance relation that should be established between implementation and specification. One commonly used confor- mance relation is the so-called input output conformance (ioco), which is defined over labeled transition systems. In this paper we investigate a denotational semantics of the input output conformance relation over reactive processes. We formalize the underlying assumptions of the ioco relation in terms of formal healthiness conditions and by adopted op- erators. Finally, we show that our denotational version of ioco can be generalized in the same way as the original relation. Our work aims to provide a unification of input output conformance by lifting the definition from labeled transition systems to reactive processes.