The notion of refinement plays an important role in software engineering. Itis the basis of a stepwise development methodology in which the correctness ofa system can be established by proving, or computing, that a system refines itsspecification. Wang et al. describe algorithms based on antichains forefficiently deciding trace refinement, stable failures refinement andfailures-divergences refinement. We identify several issues pertaining to thesoundness and performance in these algorithms and propose new, correct,antichain-based algorithms. Using a number of experiments we show that ouralgorithms outperform the original ones in terms of running time and memoryusage. Furthermore, we show that additional run time improvements can beobtained by applying divergence-preserving branching bisimulation minimisation.
展开▼
