Failure-based Congruences, Unfair Divergences and New Testing Theory

The testing equivalence 'te' that is used as a reference in verification and testing theory in LOTOS is not a congruence, and no explicit definition of the least congruence stronger than 'te' has been found. The critical LOTOS context in which congruence is lost is the hiding context that creates divergence. In this paper we first survey this problem and present three known variants of 'te' that are congruences. Each of them, as well as 'te', is then related to a particular interpretation of divergences in terms of (un)fairness of divergences. The associated preorders that generate these equivalences are also presented. Based on these results, we propose a new testing theory based on unfair divergences. It defines new equivalence and conformance relations, as well as the associated canonical tester. We also prove that the least congruence stronger than this new testing equivalence is one of three presented failure-based congruences, which thus also deserves the label of testing congruence.