Offline Trace Checking of Quantitative Properties of Service-Based Applications

TL;DR

This paper presents a method for offline verification of service-based application traces against quantitative specifications using a translation of SOLOIST into CLTLB(D) and SMT-based satisfiability checking.

Contribution

It introduces a novel translation approach from SOLOIST to CLTLB(D) for efficient offline trace checking of quantitative properties.

Findings

Effective trace checking for service applications demonstrated.

Performance comparison shows improvements over previous methods.

Applicable to various trace types and specifications.

Abstract

Service-based applications are often developed as compositions of partner services. A service integrator needs precise methods to specify the quality attributes expected by each partner service, as well as effective techniques to verify these attributes. In previous work, we identified the most common specification patterns related to provisioning service-based applications and developed an expressive specification language (SOLOIST) that supports them. SOLOIST is an extension of metric temporal logic with aggregate temporal modalities that can be used to write quantitative temporal properties. In this paper we address the problem of performing offline checking of service execution traces against quantitative requirements specifications written in SOLOIST. We present a translation of SOLOIST into CLTLB(D), a variant of linear temporal logic, and reduce the trace checking of SOLOIST to bounded satisfiability checking of CLTLB(D), which is supported by ZOT, an SMT-based verification toolkit. We detail the results of applying the proposed offline trace checking procedure to different types of traces, and compare its performance with previous work.