基于事件约束的分布式程序正确性测试

摘要

由于并发的存在和不确定性,在以规约为基础来测试分布式程序的正确性时,必须考虑程序执行时的内部状态.这些内部状态通过端口显示为事件序列,程序规约需要对序列中各事件间的依赖关系作约定,即定义事件约束集.该文提出了E-CSPE(extended-constraints on suc ceeding and preceding events),以形式化描述这类事件约束,它由3个基本描述规则组成, 分别对应于3种不同类型的事件约束.通过判断程序执行时所产生的事件序列集同这些事件约束集的一致性以及对约束集覆盖程度可以检测被测程序的正确性.