On the Unification of Conformance Notions

Most artefacts in software and system development - from software code to behavioural models - rely on conformance relations as the most important means to cope with the ever-growing complexity of today’s cyber-physical systems. There exists, however, a multitude of such relations, depending on the modelling formalisms used, from refinement relations in the CSP process algebra, via Galois connections used for abstract interpretation, to several variants of equivalence and reduction relations to be applied in finite state machine modelling. Though all intended to reduce complexity without losing essential properties, these different notions of conformance are by no means equivalent. This is because they serve different purposes and use different rules for the degrees of freedom to be allowed in a conforming artefact. The Unifying Theories of Programming provide a universal notion of conformance (called ‘refinement’ in UTP) that is based on the very basic logical requirement that the refining artefact should in some sense imply the refined artefact – possibly after hiding some observables without relevance. In this chapter, we use conformance relations that are popular in the field of finite state machines to investigate whether different important conformance notions can really be subsumed as special cases of this very liberal UTP refinement concept.