We introduce a novel methodology for testing stochastic black-box systems,
frequently encountered in embedded systems. Our approach enhances the
established black-box checking (BBC) technique to address stochastic behavior.
Traditional BBC primarily involves iteratively identifying an input that
breaches the system's specifications by executing the following three phases:
the learning phase to construct an automaton approximating the black box's
behavior, the synthesis phase to identify a candidate counterexample from the
learned automaton, and the validation phase to validate the obtained candidate
counterexample and the learned automaton against the original black-box system.
Our method, ProbBBC, refines the conventional BBC approach by (1) employing an
active Markov Decision Process (MDP) learning method during the learning phase,
(2) incorporating probabilistic model checking in the synthesis phase, and (3)
applying statistical hypothesis testing in the validation phase. ProbBBC
uniquely integrates these techniques rather than merely substituting each
method in the traditional BBC; for instance, the statistical hypothesis testing
and the MDP learning procedure exchange information regarding the black-box
system's observation with one another. The experiment results suggest that
ProbBBC outperforms an existing method, especially for systems with limited
observation.

我们介绍了一种新的测试随机黑盒系统的方法，该方法通过使用主动马尔科夫决策流程、概率模型检查和统计假设检验等技术，改进了传统的黑盒检查方法，并且在实验结果中表现优于现有方法。