Formal Verification of Web Services Composition Using Linear Logic and the pi-calculus

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


We give an overview of a rigorous approach to Web Services composition based on theorem proving in the proof assistant HOL Light. In this, we exploit the proofs-as-processes paradigm to compose multiple Web Services specified in Classical Linear Logic, while using the expressive nature of our theorem-proving framework to provide a systematic and rigorous treatment of properties such as exceptions. The end result is not only a formally verified proof of the composition, with an associated guarantee of correctness, but also an 'executable' pi-calculus statement describing the composition in process-algebraic terms. We illustrate our approach by analyzing a non-trivial example involving numerous Web Services in a real-estate domain.
Original languageEnglish
Title of host publication2011 IEEE Ninth European Conference on Web Services
Place of PublicationLos Alamitos, CA, USA
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages8
ISBN (Print)978-1-4577-1532-7
Publication statusPublished - 2011


Dive into the research topics of 'Formal Verification of Web Services Composition Using Linear Logic and the pi-calculus'. Together they form a unique fingerprint.

Cite this