Offline Trace Checking of Quantitative Properties of Service-Based Applications
This provides service integrators with a precise method to verify quality attributes in service compositions, though it is incremental as it builds on existing specification patterns and tools.
The paper tackles the problem of verifying quantitative quality attributes in service-based applications by performing offline trace checking against specifications written in SOLOIST, a metric temporal logic extension, and achieves this through translation to CLTLB(D) and SMT-based verification, with performance comparisons to prior work.
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.