Func­ti­o­nal Ana­ly­sis 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.