Model-Based Testing of Probabilistic Systems with Stochastic Time

摘要

This paper presents a model-based testing framework for black-box probabilistic systems with stochastic continuous time. Markov automata are used as an underlying model. We show how to generate, execute and evaluate test cases automatically from a probabilistically timed requirements model. In doing so, we connect classical ioco-theory with statistical hypothesis testing; our ioco-style algorithms test for functional behaviour, while X~2 hypothesis tests and confidence interval estimations assess the statistical correctness of the system. A crucial development are the classical soundness and completeness properties of our framework. Soundness states that test cases assign the correct verdict, while completeness states that our methods are powerful enough to discover each discrepancy in functional or statistical misbehaviour, up to arbitrary precision. We illustrate our framework via the Bluetooth device discovery protocol.