Most of the trace-checking tools only yield a Boolean verdict. However, when a property is violated by a trace, engineers usually inspect the trace to understand the cause of the violation; such manual diagnostic is time-consuming and error-prone. Existing approaches that complement trace-checking tools with diagnostic capabilities either produce low-level explanations that are hardly comprehensible by engineers or do not support complex signal-based temporal properties. In this paper, we propose TD-SB-TemPsy, a trace-diagnostic approach for properties expressed using SB-TemPsy-DSL. Given a property and a trace that violates the property, TD-SB-TemPsy determines the root cause of the property violation. TD-SB-TemPsy relies on the concepts of violation cause, which characterizes one of the behaviors of the system that may lead to a property violation, and diagnoses, which are associated with violation causes and provide additional information to help engineers understand the violation cause. As part of TD-SB-TemPsy, we propose a language-agnostic methodology to define violation causes and diagnoses. In our context, its application resulted in a catalog of 34 violation causes, each associated with one diagnosis, tailored to properties expressed in SB-TemPsy-DSL. We assessed the applicability of TD-SB-TemPsy on two datasets, including one based on a complex industrial case study.The results show that TD-SB-TemPsy could finish within a timeout of 1 min for ~83.66% of the trace-property combinations in the industrial dataset, yielding a diagnosis in ~99.84% of these cases. Moreover, it also yielded a diagnosis for all the trace-property combinations in the other dataset. These results suggest that our tool is applicable and efficient in most cases.

翻译：大多数轨迹检测工具仅输出布尔判定结果。然而，当轨迹违反某性质时，工程师通常需人工检查轨迹以理解违反原因——这种人工诊断既耗时又易出错。现有为轨迹检测工具补充诊断能力的方法，要么生成工程师难以理解的底层解释，要么不支持复杂的信号型时序属性。本文提出TD-SB-TemPsy——一种针对SB-TemPsy-DSL表达属性的轨迹诊断方法。给定违反性质的轨迹与性质定义，TD-SB-TemPsy可确定性质违反的根本原因。该方法基于"违反原因"（描述可能导致性质违反的系统行为）与"诊断信息"（关联违反原因并提供辅助工程师理解的附加信息）两个核心概念。作为TD-SB-TemPsy的组成部分，我们提出了一种语言无关的违反原因与诊断信息定义方法。在本研究场景下，该方法生成了34种违反原因及其对应诊断信息的目录，专门适配SB-TemPsy-DSL表达的性质。我们通过两个数据集（包含基于复杂工业案例的数据集）评估了TD-SB-TemPsy的适用性。结果表明：在工业数据集中，约83.66%的轨迹-性质组合可在1分钟超时内完成分析，其中约99.84%生成了诊断信息；而另一数据集的所有轨迹-性质组合均成功生成诊断信息。这表明我们的工具在多数场景下具备适用性与高效性。