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 using an industrial case study from the satellite domain. The results show that TD-SB-TemPsy could finish within a timeout of 1 min for ~83:66% of the trace-property combinations in our dataset, yielding a diagnosis in ~99:84% of these cases; these results suggest that our tool is applicable and efficient in most cases.
翻译:大部分跟踪检查工具仅产生布尔语判决。 但是, 当财产被跟踪破坏时, 工程师通常会检查追踪, 以了解违法行为的原因; 这种人工诊断耗时且容易出错。 现有的方法, 以诊断能力补充追踪检查工具, 要么产生工程师难以理解的低层次解释, 要么不支持基于信号的复杂时间属性。 在本文中, 我们提议TD-SB- TemPsy- DSSL, 一种对使用SB- TemPsy- DSL 表达的属性进行追踪诊断的方法。 由于财产和痕迹违反了财产, TD-SB- TemPsy 通常会检查违法行为的原因; TDSB- TemPsy 诊断: TemPSB 多数情况下, 其应用基于违反原因的概念: TDSB-L 中, 这些与违规原因有关的行为, 并提供更多信息帮助工程师了解违规原因。 作为TD-P- TemPsy 的一部分, 我们提议一种语言识别方法, 其最终结果显示SB 中的SB- true- true 。