Checking for CFFD-preorder with tester processes

This paper describes an on-the-fly technique for computing the CFFD-preorder relation on two labelled transition systems (LTSs). CFFD is a process-algebraic semantic model for comparing processes. It is a modification of the CSP model. LTSs are used as a representation of processes. The presented technique is based on transforming the specification process into a special tester process. The tester is then composed in parallel with the processes of the implementation. Violations against the specification are detected as illegal states, deadlocks and livelocks during the computation of the composition. Tester processes are an extension of Brinksma's canonical testers. Using a tester process can be a substantially faster method of computing CFFD-preorder than the previously used method of comparing acceptance graphs.