| Reference : Trace Diagnostics for Signal-based Temporal Properties |
| Scientific journals : Article | |||
| Engineering, computing & technology : Computer science | |||
| Security, Reliability and Trust | |||
| http://hdl.handle.net/10993/54317 | |||
| Trace Diagnostics for Signal-based Temporal Properties | |
| English | |
| 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 >] | |
| In press | |
| IEEE Transactions on Software Engineering | |
| Institute of Electrical and Electronics Engineers | |
| Yes | |
| International | |
| 0098-5589 | |
| 1939-3520 | |
| New-York | |
| 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 | |
| http://hdl.handle.net/10993/54317 | |
| 10.1109/TSE.2023.3242588 | |
| H2020 ; 957254 - COSMOS - DevOps for Complex Cyber-Physical Systems |
| File(s) associated to this reference | ||||||||||||||
|
Fulltext file(s):
| ||||||||||||||
All documents in ORBilu are protected by a user license.
