发表机构
FaMAF, Universidad Nacional de Córdoba; University of Twente（科尔多瓦国立大学; 特温特大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出多通道提升算子，使每个组件在各自通道上独立超时，并证明其与并行组合可交换，且保留基于模型的测试中的一致性、测试生成和判定机制。
AI 中文摘要
在基于模型的测试（MBT）中，测试套件从形式化规范中自动生成。实时系统测试的理论丰富，但在实践中常被低估，部分原因是应用定时机制需要从业者本不应具备的专业知识。在先前的工作中，我们通过一个规范提升算子解决了定时测试的这一问题，该算子允许建模者将行为指定为普通标记转换系统，同时隐式获得表达其静默行为（输出的显式缺失）并带有定时器的定时自动机。本文迈出下一步：我们证明当每个组件在其自己的通道上携带自己的超时时，我们的提升仍然有效。通过这种方式，我们引入了多通道提升。我们证明它与并行组合可交换，即先组合再提升与先提升再组合是相同的。我们证明MBT机制得以保留：一致性、测试生成和判定结果在基于超时的测试器可观察的可测试轨迹上均被提升所保留。
英文摘要
In Model-Based Testing (MBT), test suites are generated automatically from a formal specification. The theory of testing real-time systems is rich, but often underused in practice, partly because applying the timed machinery demands expertise practitioners should not need. In prior work we addressed this for timed testing with a canonic lifting operator, which lets a modeller specify behaviour as plain labelled transition systems while implicitly obtaining the timed automata that express their quiescent behaviour (the explicit absence of outputs) with timers. This paper takes the next step: we show that our lifting still works when each component carries its own time-out on its own channel. This way, we introduce a multi-channel lifting. We show that it commutes with parallel composition, i.e. composing and lifting is the same as lifting first and then composing. We show that the MBT apparatus survives: conformance, test generation and verdicts are preserved by the lifting, on the testable traces that a time-out based tester can observe.
CommentsTechnical report with proofs
