A Theory of Black-Box Tests
This provides a foundational framework for analyzing black-box testing limits, bridging testing, verification, and enforcement, though it appears incremental in formalizing existing concepts.
The paper tackles the problem of characterizing which system requirements can be refuted through black-box testing, developing a formal theory based on satisfaction and refinement. It shows that finite falsifiability of hyper-safety temporal requirements is a special case, extending the theory to computational constraints and separating refutation from enforcement.
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.