A Model-driven Approach to Trace Checking of Temporal Properties with Aggregations

By: Chaima Boufaied, Domenico Bianculli, Lionel Briand

Abstract

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 check- ing 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 ef- ficient 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 perfor- mance: 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.

Keywords

Temporal properties; Offline trace checking; Aggregation op- erators; Specification patterns; OCL.

Cite as:

Chaima Boufaied, Domenico Bianculli, Lionel Briand, “A Model-driven Approach to Trace Checking of Temporal Properties with Aggregations”, Journal of Object Technology, Volume 18, no. 2 (July 2019), pp. 15:1-21, doi:10.5381/jot.2019.18.2.a15.