基于信号的时序性质的迹诊断
软件工程
2024-08-20 v2
摘要
大多数迹检查工具仅给出布尔判定。然而，当某条迹违反性质时，工程师通常需人工检视该迹以理解违规原因；此类人工诊断耗时且易错。现有为迹检查工具补充诊断能力的方法，要么产生工程师难以理解的底层解释，要么不支持复杂的基于信号的时序性质。本文提出 TD-SB-TemPsy，一种针对使用 SB-TemPsy-DSL 表达的性质的迹诊断方法。给定一个性质及一条违反该性质的迹，TD-SB-TemPsy 确定性质违反的根因。TD-SB-TemPsy 依赖于违规原因（violation cause）的概念——其刻画了可能导致性质违反的系统行为之一，以及诊断（diagnoses）——其与违规原因相关联并提供附加信息以帮助工程师理解违规原因。作为 TD-SB-TemPsy 的一部分，我们提出一种与语言无关的方法来定义违规原因与诊断。在我们的语境下，其应用产生了一个包含 34 个违规原因的目录，每个原因关联一个诊断，专为 SB-TemPsy-DSL 表达的性质定制。我们在两个数据集上评估了 TD-SB-TemPsy 的适用性，其中一个基于复杂的工业案例研究。结果显示，TD-SB-TemPsy 在工业数据集中约 83.66% 的迹-性质组合上能在 1 分钟超时内完成，并在其中约 99.84% 的案例给出诊断。此外，它对另一数据集中的所有迹-性质组合也都给出了诊断。这些结果表明我们的工具在大多数情况下具有适用性与高效性。
引用
@article{arxiv.2206.04024,
title = {Trace Diagnostics for Signal-based Temporal Properties},
author = {Chaima Boufaied and Claudio Menghi and Domenico Bianculli and Lionel Briand},
journal= {arXiv preprint arXiv:2206.04024},
year = {2024}
}