Sie haben Javascript deaktiviert!
Sie haben versucht eine Funktion zu nutzen, die nur mit Javascript möglich ist. Um sämtliche Funktionalitäten unserer Internetseite zu nutzen, aktivieren Sie bitte Javascript in Ihrem Browser.

CRC 901 – On-The-Fly Computing (OTF Computing)

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.

Die Universität der Informationsgesellschaft