Universität Paderborn » SFB 901 » Projects » Tools & Demonstration Systems » Functional Analysis Tools

Functional Analysis Tools


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


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.


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