Gerhold and Stoelinga’s paper proposes an interesting framework to test probabilistic systems based on the concepts of soundness and completeness. The crux of their argument is “the conformance relation for probabilistic input/output conformance” (ioco), which informs “exactly when an implementation should pass a test.” Soundness here means a proper implementation is that which passes a test suite, while completeness means the framework is capable of detecting each deviation from a specification sufficiently precisely, at least for large samples.

The authors show “how to automatically derive, execute, and evaluate probabilistic test cases” as per the mode requirement. Three illustrative case studies are presented, namely, “Knuth and Yao’s dice application, the binary exponential backoff protocol, and the FireWire leadership protocol.” The implementation of the test evaluation processes turns out to be functionally and statistically correct.

This is a nicely written paper that I would certainly recommend for postgraduates and researchers in statistics and computer science.