A Theory of Black-Box Tests

TL;DR

This paper develops a formal theory of black-box testing based on satisfaction and refinement, characterizing what requirements can be refuted or verified through such tests, including hyper-safety temporal properties.

Contribution

It introduces a formal framework for understanding the scope of black-box tests, including finite refutability and the separation of refutation from enforcement in temporal hyper-properties.

Findings

Finite falsifiability of hyper-safety temporal requirements

Characterization of refutable and verifiable requirements via black-box testing

Extension of the theory with computational constraints

Abstract

The purpose of testing a system with respect to a requirement is to refute the hypothesis that the system satisfies the requirement. We build a theory of tests and refutation based on the elementary notions of satisfaction and refinement. We use this theory to characterize the requirements that can be refuted through black-box testing and, dually, verified through such tests. We consider refutation in finite time and obtain the finite falsifiability of hyper-safety temporal requirements as a special case. We extend our theory with computational constraints and separate refutation from enforcement in the context of temporal hyper-properties. Overall, our theory provides a basis to analyze the scope and reach of black-box tests and to bridge results from diverse areas including testing, verification, and enforcement.