Failure trace (or refusal trace) semantics is arguably the finest semantics that admits a realistic testing scenario, though the testing community has traditionally favoured coarser relations such as failures, traces, ioco etc.

In my talk, I will discuss our recent work on finding a minimal complete test suite for failure trace refinement. Simply put, we wish to determine, for a given process P, a minimal set of failure traces TS(P) such that every process Q that does not refine P, exhibits some trace in TS(P).

Our solution utilises several interesting insights into the nature of refusal/failure traces. In particular, we identify a natural equivalence relation on refusals called cluster equivalence; its equivalence classes can only be exhibited by conforming systems as a whole. Moreover, we provide an exact characterisation of redundant traces in a test suite, identifying in particular a singular class of traces that can be omitted from the suite due to the testing power of longer traces. Omitting traces in such cases is debatable, however, hence our complete test suites come in two variants — in both instances being minimal.

A related problem from the realm of modal logic is the construction of a characteristic formula of a given process P, that is, a formula Φ(P) such that every process which satisfies Φ(P) refines P. Our test generation scheme can be used to construct such a formula using a variant of Hennessy-Milner logic with recursion.