关于时态: 建模通过时限实现的测试中静止行为
形式语言与自动机理论
2025-07-25 v1
摘要
基于模型的测试 (MBT) 从系统under test 的行为规范中派生测试套件。在实际中，工程师倾向于使用简单模型，如标记迹移系统 (LTS)。然而，为处理静止性 - 输出的不可见性 - 实践中需要设置时限以确定静止性的观察结束。时态 MBT 存在，但通常依赖于时态自动机 (TA) 的完整工具箱。我们提出了 lifting operator ，用于在不引入 TA 负担的情况下添加时序性质：给定 LTS， 引入一个用于用户选择的时限 的单个时钟，以声明静止性。在时态自动机中，该时钟用于建模输出应在时钟到达值 之前发生，而静止性恰好发生在时间 。因此，我们为工业实践中选择时限以确定静止性提供了形式化基础。我们的贡献有三点：(1) 一个实现在 下符合当且仅当其提升版本在带时限的 下符合 (2) 在或之后应用 之前的标准 测试生成算法与之后的应用结果相同的测试集 (3) 提升后的时态自动机测试套件和原始 LTS 测试套件为每个实现提供相同的裁决。
引用
@article{arxiv.2507.18205,
title = {Time for Quiescence: Modelling quiescent behaviour in testing via time-outs in timed automata},
author = {Laura Brandán Briones and Marcus Gerhold and Petra van den Bos and Mariëlle Stoelinga},
journal= {arXiv preprint arXiv:2507.18205},
year = {2025}
}