Maurice Laveaux: Antichain Based Algorithm for Fair Testing

Event Details

The notion of refinement plays an important role in software engineering. It is the basis of a stepwise development methodology in which the correctness of a system can be established by proving, or computing, that a system refines its specification. There are many refinement relations described in the literature. Fair testing is the coarsest liveness-preserving refinement relation that is a precongruence for a CSP inspired process algebra. The main feature of fair testing is that it abstracts from divergences in the same way as Milner’s observation congruence, and as a result is also strictly coarser than observation congruence. This can be seen as a built-in fairness assumption. Fair testing has been shown to be decidable, but its algorithm is not yet practical. In this presentation I will describe fair testing and the algorithm. Furthermore, I will also explain the applicability of antichains to improve the efficiency of the algorithm.