输入输出一致性测试中的组合性、分解性与精化——技术报告

我们提出一种输入输出一致性测试理论，利用带有输入拒绝的模态接口自动机(IR-MIA)作为规约和被测实现的新型行为形式化。IR-MIA上的模态精化关系允许区分义务性和允许的输出行为，以及隐式未指定和显式禁止的输入行为。因此该理论支持具有乐观和悲观环境假设的积极和消极一致性测试。我们进一步展示所得IR-MIA上的一致性关系（称为modal-irioco）享有许多关于基于组件行为的期望性质。首先，modal-irioco在模态精化下保持，并在某些限制下构成预序，这些限制可通过IR-MIA的规范输入补全确保。其次，在相同限制下，modal-irioco关于IR-MIA的并行组合与多播和隐藏是组合的。最后，IR-MIA上的商算子作为并行组合的逆，促进一致性测试中的可分解性以解决未知组件问题。