概率自动机的 ioco 理论

基于模型的测试（MBT）是一种众所周知的技术，允许自动生成、执行和评估测试用例。为了测试非功能属性，已开发了许多 MBT 测试框架来测试具有实时、连续行为、符号数据和定量系统方面的系统。值得注意的是，这些框架中有许多基于 Tretmans 的经典输入输出一致性（ioco）框架。然而，处理概率行为的基于模型的测试理论尚不存在。概率在许多不同系统中起作用：不可靠的通信信道、随机算法和通信协议、确定正常运行时间百分比的服务水平协议等。因此，概率测试理论具有重要的实际意义。我们提出了 ioco 的概率变体的要素，并定义了 {\pi}oco 关系，证明其保守地扩展 ioco，并定义了测试用例、执行和评估的概念。