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

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.