Mutually Testing Processes

TL;DR

This paper explores a unified framework for process refinement preorders, including server-client and peer-to-peer settings, providing behavioral and equational characterizations for finite processes.

Contribution

It introduces a uniform account of multiple process refinement preorders, extending standard testing theory to peer processes with behavioral and equational characterizations.

Findings

Characterizations of preorders via traces and ready sets

Equational characterization for finite processes

Unified framework for server, client, and peer process refinements

Abstract

In the standard testing theory of DeNicola-Hennessy one process is considered to be a refinement of another if every test guaranteed by the former is also guaranteed by the latter. In the domain of web services this has been recast, with processes viewed as servers and tests as clients. In this way the standard refinement preorder between servers is determined by their ability to satisfy clients. But in this setting there is also a natural refinement preorder between clients, determined by their ability to be satisfied by servers. In more general settings where there is no distinction between clients and servers, but all processes are peers, there is a further refinement preorder based on the mutual satisfaction of peers. We give a uniform account of these three preorders. In particular we give two characterisations. The first is behavioural, in terms of traces and ready sets. The second, for finite processes, is equational.