A theorem proving framework for the formal verification of Web Services Composition

TL;DR

This paper introduces a formal framework using higher order logic and pi-calculus for the rigorous, sound, and correct composition of Web Services, leveraging proofs-as-processes and Classical Linear Logic.

Contribution

It presents a novel theorem proving approach for Web Services composition that ensures soundness and correctness through formal logic and process extraction.

Findings

Framework implemented in HOL Light

Supports multiple Web Services properties in composition

Guarantees soundness and correctness

Abstract

We present a rigorous framework for the composition of Web Services within a higher order logic theorem prover. Our approach is based on the proofs-as-processes paradigm that enables inference rules of Classical Linear Logic (CLL) to be translated into pi-calculus processes. In this setting, composition is achieved by representing available web services as CLL sentences, proving the requested composite service as a conjecture, and then extracting the constructed pi-calculus term from the proof. Our framework, implemented in HOL Light, not only uses an expressive logic that allows us to incorporate multiple Web Services properties in the composition process, but also provides guarantees of soundness and correctness for the composition.