Reference : Trace Diagnostics for Signal-based Temporal Properties
Scientific journals : Article
Engineering, computing & technology : Computer science
Security, Reliability and Trust
Trace Diagnostics for Signal-based Temporal Properties
Boufaied, Chaima [University of Ottawa]
Menghi, Claudio []
Bianculli, Domenico mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV >]
Briand, Lionel mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV >]
In press
IEEE Transactions on Software Engineering
Institute of Electrical and Electronics Engineers
United States - New York
[en] diagnostics ; trace checking ; runtime verification ; temporal properties ; specification patterns ; cyber-physical systems
[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.
Interdisciplinary Centre for Security, Reliability and Trust (SnT) > SVV - Software Verification and Validation
European Commission - EC
Researchers ; Professionals
H2020 ; 957254 - COSMOS - DevOps for Complex Cyber-Physical Systems

File(s) associated to this reference

Fulltext file(s):

Open access
main.pdfAuthor postprint1.04 MBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.