Func­tion­al Ana­lys­is Tools

Overview

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

Fea­tures

Functional analysis is enabled for two main properties:

  • Protocol-based analysis: Deadlock-freedom, protocol-adherence
  • Semantic analysis: Adherence to required pre- and postconditions, taking formalized domain knowledge into account

In a first step, SSL specifications of a 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.

Related Tools

  • The Spin model checker is used for protocol-based verification.
  • The Z3 SMT solver is used for pre-/postcondition-based verification.

Contact

If you have any questions regarding Functional Analysis Tools, contact research staff from Subproject B3.

Further information:

Projects Project Area A Project Area B Project Area C Project Area T Tools and Demonstration Systems Tools from the 1st Funding Period Tools from the 2nd Funding Period Tools from the 3rd Funding Period