Achtung:

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.

SFB 901 - On-The-Fly Computing
  • Kontakt
  • EN | DE
CRC 901 – On-The-Fly Computing (OTF Computing) Bildinformationen anzeigen

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

Functional Analysis Tools

Bild vergrößern

Overview

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

Features

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.

Sie interessieren sich für:

Die Universität der Informationsgesellschaft