Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Trace Diagnostics for Signal-based Temporal Properties

Chaima Boufaied, Claudio Menghi, Domenico Bianculli, Lionel Briand

TL;DR

TD-SB-TemPsy addresses the lack of diagnostic support for signal-based temporal properties by introducing violation causes and diagnoses and a language-agnostic methodology to define them, specialized to SB-TemPsy-DSL. It provides a catalog of 34 violation causes, each paired with a diagnosis that reveals concise, actionable trace evidence. The approach is implemented as a SB-TemPsy-Check plugin and evaluated on a large industrial PROP-SAT satellite dataset and on the AFC benchmark, demonstrating practical applicability within realistic timeouts and high diagnostic coverage. The work offers a reusable framework for trace diagnostics in pattern-based specifications and can guide extensions to other DSLs such as TemPsy and FRETISH, with potential impact on fault localization in CPS.

Abstract

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.

Trace Diagnostics for Signal-based Temporal Properties

TL;DR

TD-SB-TemPsy addresses the lack of diagnostic support for signal-based temporal properties by introducing violation causes and diagnoses and a language-agnostic methodology to define them, specialized to SB-TemPsy-DSL. It provides a catalog of 34 violation causes, each paired with a diagnosis that reveals concise, actionable trace evidence. The approach is implemented as a SB-TemPsy-Check plugin and evaluated on a large industrial PROP-SAT satellite dataset and on the AFC benchmark, demonstrating practical applicability within realistic timeouts and high diagnostic coverage. The work offers a reusable framework for trace diagnostics in pattern-based specifications and can guide extensions to other DSLs such as TemPsy and FRETISH, with potential impact on fault localization in CPS.

Abstract

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.
Paper Structure (37 sections, 8 equations, 16 figures, 2 tables, 2 algorithms)

This paper contains 37 sections, 8 equations, 16 figures, 2 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Case Study and Motivations
  3. Background: SB-TemPsy-DSL
  4. Pattern-based trace diagnostic
  5. Methodology for Defining Violation Causes and Diagnoses
  6. Behavior Analysis
  7. Definition of Violation Causes
  8. Definition of diagnoses
  9. Properties of the methodology
  10. Violation Causes and Diagnoses for SB-TemPsy-DSL
  11. Patterns
  12. assert: Event-based Data Assertion
  13. becomes: State-based Data Assertion
  14. Spike
  15. Oscillation
  16. ...and 22 more sections

Figures (16)

  • Figure 1: A fragment of a trace from our case study.
  • Figure 2: Graphical representation of the trace in Figure \ref{['fig:traceExample']}.
  • Figure 3: SB-TemPsy-DSL syntax.
  • Figure 4: SB-TemPsy-DSL formal semantics (based on boufaied2020trace)
  • Figure 5: A trace with signals violating the expression "existsspikein$\beta$withwidth < 0.5 amplitude < 90".
  • ...and 11 more figures