Article (Scientific journals)
Trace Diagnostics for Signal-based Temporal Properties
Boufaied, Chaima; Menghi, Claudio; Bianculli, Domenico et al.
2023In IEEE Transactions on Software Engineering, 49 (5), p. 3131-3154
Peer Reviewed verified by ORBi


Full Text
Author postprint (1.07 MB)

All documents in ORBilu are protected by a user license.

Send to


Keywords :
diagnostics; trace checking; runtime verification; temporal properties; specification patterns; cyber-physical systems
Abstract :
[en] Trace checking is a verification technique widely used in Cyber-physical system (CPS) development, to verify whether execution traces satisfy or violate properties expressing system requirements. Often these properties characterize complex signal behaviors and are defined using domain-specific languages, such as SB-TemPsy-DSL, a pattern-based specification language for signal-based temporal properties. 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.
Research center :
Interdisciplinary Centre for Security, Reliability and Trust (SnT) > SVV - Software Verification and Validation
Disciplines :
Computer science
Author, co-author :
Boufaied, Chaima;  University of Ottawa
Menghi, Claudio
Bianculli, Domenico  ;  University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV
Briand, Lionel ;  University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV
External co-authors :
Language :
Title :
Trace Diagnostics for Signal-based Temporal Properties
Publication date :
May 2023
Journal title :
IEEE Transactions on Software Engineering
Publisher :
Institute of Electrical and Electronics Engineers, New-York, United States - New York
Volume :
Issue :
Pages :
Peer reviewed :
Peer Reviewed verified by ORBi
Focus Area :
Security, Reliability and Trust
European Projects :
H2020 - 957254 - COSMOS - DevOps for Complex Cyber-physical Systems
Funders :
CE - Commission Européenne [BE]
Available on ORBilu :
since 01 February 2023


Number of views
63 (17 by Unilu)
Number of downloads
49 (7 by Unilu)

Scopus citations®
Scopus citations®
without self-citations
WoS citations


Similar publications

Contact ORBilu