The ever-growing complexity of today's soft-and hardware makes testing both an indispensable necessityand a challenging task. At the given scale, manual testing is unfeasible, which raises the urge for automated approaches. At the same time, the ongoing digitalization ofsecurity-and safety-centric applications requires exhaustive verification of key properties. A field of research that tackles these problems and has yielded sophisticating results is that of model-based testing [Bro 05] and model checking [BK08]. Formal verification methods, depending on the scenario, allow the automated generation of tests or the automated evaluation of test properties. Being based on formal models, a successful verification is also able to provably guarantee certain properties of the system under testing. Key to a successful application of these techniques is a formal specification of the target system. This requirement, however, poses a problem to many real-world applications: Thelack of formal specifications for software or hardware hinders the employment of formal verification methods. Creating formal specifications for soft-or hardware components is not only a tedious task but also prone to errors.

Substitutability, interchangeability and related concepts in Constraint Programming were introduced approximately twenty years ago and have given rise to considerable subsequent research. We survey this work, classify, and relate the different concepts, and indicate directions for future work, in particular with respect to making connections with research into symmetry breaking. This paper is a condensed version of a larger work in progress.