Reference : Trace-Checking Signal-based Temporal Properties: A Model-Driven Approach
Scientific congresses, symposiums and conference proceedings : Paper published in a book
Engineering, computing & technology : Computer science
Security, Reliability and Trust
http://hdl.handle.net/10993/44159
Trace-Checking Signal-based Temporal Properties: A Model-Driven Approach
English
Boufaied, Chaima mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Menghi, Claudio mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Bianculli, Domenico mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Briand, Lionel mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Isasi Parache, Yago []
Sep-2020
Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering (ASE ’20)
Yes
No
International
35th IEEE/ACM International Conference on Automated Software Engineering (ASE ’20)
from 21-09-2020 to 25-09-2020
[en] trace checking ; run-time verification ; temporal properties ; specification patterns ; model-driven ; cyber-physical systems ; signals
[en] Signal-based temporal properties (SBTPs) characterize the behavior of a system when its inputs and outputs are signals over time; they are very common for the requirements specification of cyber-physical systems. Although there exist several specification languages for expressing SBTPs, such languages either do not easily allow the specification of important types of properties (such as spike or oscillatory behaviors), or are not supported by (efficient) trace-checking procedures.

In this paper, we propose SB-TemPsy, a novel model-driven trace-checking approach for SBTPs. SB-TemPsy provides (i) SB-TemPsy-DSL, a domain-specific language that allows the specification of SBTPs covering the most frequent requirement types in cyber-physical systems, and (ii) SB-TemPsy-Check, an efficient, model-driven trace-checking procedure. This procedure reduces the problem of checking an SB-TemPsy-DSL property over an execution trace to the problem of evaluating an Object Constraint Language constraint on a model of the execution trace.

We evaluated our contributions by assessing the expressiveness of SB-TemPsy-DSL and the applicability of SB-TemPsy-Check using a representative industrial case study in the satellite domain. SB-TemPsy-DSL could express 97% of the requirements of our case study and SB-TemPsy-Check yielded a trace-checking verdict in 87% of the cases, with an average checking time of 48.7 s. From a practical standpoint and compared to state-of-the-art alternatives, our approach strikes a better trade-off between expressiveness and performance as it supports a large set of property types that can be checked, in most cases, within practical time limits.
Interdisciplinary Centre for Security, Reliability and Trust (SnT) > Software Verification and Validation Lab (SVV Lab) ; University of Luxembourg: High Performance Computing - ULHPC
European Commission - EC ; University of Luxembourg - UL
R-AGR-0731-00
Researchers ; Professionals
http://hdl.handle.net/10993/44159
H2020 ; 694277 - TUNE - Testing the Untestable: Model Testing of Complex Software-Intensive Systems

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
ase2020.pdfAuthor postprint1.25 MBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.