Finite Axiom Systems for Testing Preorder and De Simone Process Languages

We prove that testing preorder of De Nicola and Hennessy is preserved by all De Simone process operators. Based on this result we propose an algorithm for generating axiomatisations of testing preorder for arbitrary De Simone process languages. The axiom systems produced by our algorithm are finite and complete for processes with finite behaviour. In order to achieve completeness for a subclass of processes with infinite behaviour we use one infinitary induction rule. The usefulness of our results is illustrated in specification and verification of small concurrent systems, where suspension, resumption and alternation of execution of component systems occur. We argue that better specifications can be more easily written in custom-made De Simone process languages which contain both the standard operators as well as new, specially tailored for the task in hand De Simone operators. Moreover, the automatically generated axiom systems for such specification languages make the verification s..