Conformance relation, associated equivalence, and minimum canonical tester in LOTOS

We first study the conf relation proposed by E. Brinksma and G. Scollo to formalise testing conformance. It is well-known from their work that, in order to test whether an implementation of a specification S (i.e. I conf S), it suffices to build, from S, a canonical tester T(S) such that, when T(S) is synchronised with an implementation I, it always reaches a correct final state if, and only if, I conf S. For instance, if I is not a valid implementation of S, the canonical tester T(S) may deadlock with I before reaching a correct final state. We put into evidence the role of the equivalence relation, conf-eq, associated naturally with conf. An important result states that if S1 conf S2, their canonical testers T1 and T2 must also satisfy T1 conf-eq T2, and reversely. Therefore, the best approach is to define the canonical tester modulo conf-eq, whereas it is currently defined modulo the testing equivalence te. Taking into account that conf-eq is weaker than te, we were able to propose a minimum canonical tester which is simpler than T(S): unlike T(S), it may have fewer traces than the specification S. The term minimum means that no trace from this tester can be deleted without losing the exhaustive test property or, stated otherwise, without taking the risk of accepting an invalid implementation (in the conf sense).