Paper published in a journal (Scientific congresses, symposiums and conference proceedings)
A Model-driven Approach to Trace Checking of Temporal Properties with Aggregations
Boufaied, Chaima; Bianculli, Domenico; Briand, Lionel
2019In Journal of Object Technology, 18 (2), p. 15:1-21
Peer Reviewed verified by ORBi
 

Files


Full Text
ecmfa2019.pdf
Author postprint (630.52 kB)
Download

All documents in ORBilu are protected by a user license.

Send to



Details



Keywords :
temporal properties; offline trace checking; aggregation operators; specification patterns; OCL
Abstract :
[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.
Research center :
Interdisciplinary Centre for Security, Reliability and Trust (SnT) > Software Verification and Validation Lab (SVV Lab)
Disciplines :
Computer science
Author, co-author :
Boufaied, Chaima ;  University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
Bianculli, Domenico  ;  University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
Briand, Lionel ;  University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
External co-authors :
no
Language :
English
Title :
A Model-driven Approach to Trace Checking of Temporal Properties with Aggregations
Publication date :
July 2019
Event name :
15th European Conference on Modelling Foundations and Applications (ECMFA)
Event place :
Eindhoven, Netherlands
Event date :
July 15-19 2019
Audience :
International
Journal title :
Journal of Object Technology
ISSN :
1660-1769
Publisher :
AITO
Volume :
18
Issue :
2
Pages :
15:1-21
Peer reviewed :
Peer Reviewed verified by ORBi
Focus Area :
Security, Reliability and Trust
European Projects :
H2020 - 694277 - TUNE - Testing the Untestable: Model Testing of Complex Software-Intensive Systems
Funders :
University of Luxembourg - UL
CE - Commission Européenne [BE]
Available on ORBilu :
since 09 June 2019

Statistics


Number of views
298 (47 by Unilu)
Number of downloads
308 (64 by Unilu)

Scopus citations®
 
3
Scopus citations®
without self-citations
1
OpenCitations
 
4
WoS citations
 
3

Bibliography


Similar publications



Contact ORBilu