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.
- 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.