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

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

Abstract

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)
Pages31-38
Number of pages8
ISBN (Print)978-1-4577-1532-7
DOIs
Publication statusPublished - 2011

Fingerprint

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