Finite Axiom Systems for Testing Preorder and De Simone Process Languages,
This is a slightly extended and updated version of an abstract which appeared in the Proceedings of the 5th International Conference on Algebraic Methodology and Software Technology AMAST'96, 1996, Springer-Verlag, LNCS 1101.
We propose a procedure for generating finite axiomatisations of testing preorder of De Nicola and Hennessy for De Simone process language. We also prove that testing preorder is preserved by all De Simone process operators. The usefulness of our results is illustrated in specification and verification of a (small) multi-media system. The important features of the system are suspension, resumption and alternation of execution of its components. We argue that the ability to use specially tailored De Simone operators allows to write clear and intuitive specifications. Moreover, the automatically generated axioms for such operators make the verification straightforward.