Reference : Specification and Model-driven Trace Checking of Complex Temporal Properties
Dissertations and theses : Doctoral thesis
Engineering, computing & technology : Computer science
Security, Reliability and Trust
Specification and Model-driven Trace Checking of Complex Temporal Properties
Boufaied, Chaima mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV >]
University of Luxembourg, ​Kirchberg, ​​Luxembourg
Docteur en Informatique
Bianculli, Domenico mailto
Pastore, Fabrizio mailto
Briand, Lionel mailto
SAN PIETRO, Pierluigi mailto
Inverardi, Paola mailto
[en] Trace checking ; runtime verification ; temporal properties
[en] Offline trace checking is a procedure used to evaluate requirement properties over a
trace of recorded events. System properties verified in the context of trace checking can be
specified using different specification languages and formalisms; in this thesis, we consider
two classes of complex temporal properties: 1) properties defined using aggregation operators;
2) signal-based temporal properties from the Cyber Physical System (CPS) domain.
The overall goal of this dissertation is to develop methods and tools for the specification
and trace checking of the aforementioned classes of temporal properties, focusing on the
development of scalable trace checking procedures for such properties.
The main contributions of this thesis are:
i) the TEMPSY-CHECK-AG model-driven approach for trace checking of temporal properties
with aggregation operators, defined in the TemPsy-AG language;
ii) a taxonomy covering the most common types of Signal-based Temporal Properties (SBTPs)
in the CPS domain;
iii) SB-TemPsy, a trace-checking approach for SBTPs that strikes a good balance in industrial
contexts in terms of efficiency of the trace checking procedure and coverage of the most
important types of properties in CPS domains. SB-TemPsy includes: 1) SB-TemPsy-DSL,
a DSL that allows the specification of the types of SBTPs identified in the aforementioned
taxonomy, and 2) an efficient trace-checking procedure, implemented in a prototype
tool called SB-TemPsy-Check;
iv) TD-SB-TemPsy-Report, a model-driven trace diagnostics approach for SBTPs expressed
in SB-TemPsy-DSL. TD-SB-TemPsy-Report relies on a set of diagnostics patterns, i.e., undesired
signal behaviors that might lead to property violations. To provide relevant and
detailed information about the cause of a property violation, TD-SB-TemPsy-Report determines
the diagnostics information specific to each type of diagnostics pattern.
Our technological contributions rely on model-driven approaches for trace checking and
trace diagnostics. Such approaches consist in reducing the problem of checking (respectively,
determining the diagnostics information of) a property over an execution trace to the
problem of evaluating an OCL (Object Constraint Language) constraint (semantically equivalent
to ) on an instance (equivalent to ) of a meta-model of the trace. The results — in
terms of efficiency of our model-driven tools—presented in this thesis are in line with those
presented in previous work, and confirm that model-driven technologies can lead to the development
of tools that exhibit good performance from a practical standpoint, also when
applied in industrial contexts.
Interdisciplinary Centre for Security, Reliability and Trust (SnT) > Software Verification and Validation Lab (SVV Lab)
University of Luxembourg - UL
Researchers ; Professionals ; General public
H2020 ; 694277 - TUNE - Testing the Untestable: Model Testing of Complex Software-Intensive Systems

File(s) associated to this reference

Fulltext file(s):

Open access
thesis_chaimaBoufaied.pdfAuthor postprint1.76 MBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.