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

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationProceedings 7th International Workshop on Automated Specification and Verification of Web Systems, Reykjavik, Iceland, 9th June 2011
EditorsLaura Kovacs, Rosario Pugliese, Francesco Tiezzi
PublisherOpen Publishing Association
Number of pages16
Publication statusPublished - 2011

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
ISSN (Electronic)2075-2180


Dive into the research topics of 'A theorem proving framework for the formal verification of Web Services Composition'. Together they form a unique fingerprint.

Cite this