Just Testing

TL;DR

This paper introduces a new must-testing preorder based on justness as the completeness criterion, using Petri nets with read arcs to model systems and connecting to fair failure preorder concepts.

Contribution

It defines a novel must-testing preorder using justness, characterizes it as the fair failure preorder, and applies Petri nets with read arcs to process algebra semantics.

Findings

The new must-testing preorder is incomparable with the traditional one.

It is the coarsest precongruence preserving linear time properties under justness.

Petri nets with read arcs effectively model process algebra with signals.

Abstract

The concept of must testing is naturally parametrised with a chosen completeness criterion, defining the complete runs of a system. Here I employ justness as this completeness criterion, instead of the traditional choice of progress. The resulting must-testing preorder is incomparable with the default one, and can be characterised as the fair failure preorder of Vogler. It also is the coarsest precongruence preserving linear time properties when assuming justness. As my system model I here employ Petri nets with read arcs. Through their Petri net semantics, this work applies equally well to process algebras. I provide a Petri net semantics for a standard process algebra extended with signals; the read arcs are necessary to capture those signals.