Testing theory in a functional process algebra

In this paper we present an algebra of processes with input and output. The key point is the conceptual distinction between input and output actions.We give an operational semantics and a notion of testing where the experimenter is not allowed to restrict the output possibilities of the process under test, as it instead could be the case if the standard synchronization-based approach of process algebra would be used. We also give two denotational models, one based on la kind of acceptance trees and the other based on sets of functions and we prove them fully abstract with respect to the testing equivalence induced by the new notion of experimenter. The model based on sets of functions provides a simple and powerful way for combining the process algebra approach with the functional one. In process algebras notions for dealing with non--determinism and progress properties of processes deadlock, etc. has been studied deeply. In thefunctional approach clean proof styles - like the transformational one -- and proof techniques - like induction principles for minimal as well as maximal fixpoints - have been proved successful. The combination of these approaches gives an interesting framework for the specification and verification A of concurrent systems.