This tool provides functional analysis of service compositions based on the SSL specification language.

Overview

The Functional Analysis is performed to analyse service compositions for adherence to specified pre- and post-conditions. Figure 1. briefly describes our approach. Subproject  B2 generates a composition of different services. In the first step, the SSL specifications of the service composition and its requirements are translated into an intermediate model, depending on the exact formalism. After that, external off-the-shelf tools are used for verification and the result transferred back to B2. So far, we have implemented three approaches for analysing service compositions, one based on the computation of strongest post-conditions, one for error localization based on Max-SAT and an approach for template verification. The first two approaches work by analysing the logical encoding of the control flow (data model) which is generated from the service composition. The third approach first of all verifies the correctness of templates (workflow descriptions) and based on this can show correctness of instantiations.