	computer science
	HOME	MAP	CONTACT

Finite Axiom Systems for Testing Preorder and De Simone Process Languages,
Irek Ulidowski,
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.

Abstract

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.

\| \|\|\|\|\|\|\|\|
Author: Irek Ulidowski (I.Ulidowski@mcs.le.ac.uk). © University of Leicester. Last modified: 13th January 2004, 16:46:15 CS Web Maintainer.

computer science