Search-based Trace Diagnostic

TL;DR

The paper tackles the problem of explaining CPS requirement violations by analyzing execution traces with signal-based temporal properties. It introduces Search-based Trace-Diagnostic (SBTD), an evolutionary framework that dynamically mutates CPS requirements, checks them against traces, and generates diagnosis via a change-driven approach and a learned decision tree. Implemented as Diagnosis for Hybrid Logic of Signals (HLS), the method demonstrates high effectiveness (33/34 informative diagnoses) and practical efficiency across automotive and robotic benchmarks, while acknowledging limitations of trace-checkers and ML-based explanations. This work offers a library-free, scalable pathway to understand trace violations, with strong implications for CPS verification and fault diagnosis in industrial contexts.

Abstract

Cyber-physical systems (CPS) development requires verifying whether system behaviors violate their requirements. This analysis often considers system behaviors expressed by execution traces and requirements expressed by signal-based temporal properties. When an execution trace violates a requirement, engineers need to solve the trace diagnostic problem: They need to understand the cause of the breach. Automated trace diagnostic techniques aim to support engineers in the trace diagnostic activity. This paper proposes search-based trace-diagnostic (SBTD), a novel trace-diagnostic technique for CPS requirements. Unlike existing techniques, SBTD relies on evolutionary search. SBTD starts from a set of candidate diagnoses, applies an evolutionary algorithm iteratively to generate new candidate diagnoses (via mutation, recombination, and selection), and uses a fitness function to determine the qualities of these solutions. Then, a diagnostic generator step is performed to explain the cause of the trace violation. We implemented Diagnosis, an SBTD tool for signal-based temporal logic requirements expressed using the Hybrid Logic of Signals (HLS). We evaluated Diagnosis by performing 34 experiments for 17 trace-requirements combinations leading to a property violation and by assessing the effectiveness of SBTD in producing informative diagnoses and its efficiency in generating them on a time basis. Our results confirm that Diagnosis can produce informative diagnoses in practical time for most of our experiments (33 out of 34).

Figures (11)

• Figure 1: Example of failure-revealing scenario.
• Figure 2: Syntax of HLS.
• Figure 3: A fragment of an execution trace for our case study.
• Figure 4: The search-based trace-diagnostic framework.
• Figure 5: Diagnosis generated for our automotive example.

Theorems & Definitions (1)

• Definition 1: Change-Driven Diagnosis