Reference : A Model-driven Approach to Trace Checking of Temporal Properties with Aggregations
Scientific congresses, symposiums and conference proceedings : Paper published in a journal
Engineering, computing & technology : Computer science
Security, Reliability and Trust
http://hdl.handle.net/10993/39639
A Model-driven Approach to Trace Checking of Temporal Properties with Aggregations
English
Boufaied, Chaima 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) > >]
In press
Journal of Object Technology
AITO
18
2
15:1-20
Yes (verified by ORBilu)
No
International
1660-1769
15th European Conference on Modelling Foundations and Applications (ECMFA)
July 15-19 2019
Eindhoven
The Netherlands
[en] temporal properties ; offline trace checking ; aggregation operators ; specification patterns ; OCL
[en] The verification of complex software systems often requires to check quantitative properties that rely on aggregation operators (e.g., the average response time of a service). One way to ease the specification of these properties is to use property specification patterns, such as the ones for “service provisioning”, previously proposed in the literature.
In this paper we focus on the problem of performing offline trace checking of temporal properties containing aggregation operators. We first present TemPsy-AG, an extension of TemPsy—an existing pattern-based language for the specification of temporal properties—to support service provisioning patterns that use aggregation operators. We then extend an existing model-driven procedure for trace checking, to verify properties expressed in TemPsy-AG. The trace checking procedure relies on the efficient mapping of temporal properties written in TemPsy-AG into OCL constraints on a meta-model of execution traces. We have implemented this procedure in the TemPsy-Check-AG tool and evaluated its performance: our approach scales linearly with respect to the length of the input trace and can deal with much larger traces than a state-of-the-art tool.
Interdisciplinary Centre for Security, Reliability and Trust (SnT) > Software Verification and Validation Lab (SVV Lab)
University of Luxembourg - UL ; European Commission - EC
http://hdl.handle.net/10993/39639
10.5381/jot.2019.18.2.a15
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
ecmfa2019.pdfAuthor postprint615.74 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.