Diagrammatically-Driven Formal Verification of Web-Services Composition

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


This paper describes a diagrammatic approach to the formal verification of web-services composition. We present a set of graphical composition rules that map to proof steps in Classical Linear Logic (CLL) and can be used to drive the proof assistant HOL Light purely through interactive, diagrammatic reasoning. The end result is a verified, workflow-like diagram that provides a visual account of the composition process and of the information flow between the services making up the composite service. Our approach thus removes the need to interact directly with HOL Light and provides a mean of visualising and carrying out the whole verification process at an intuitive, yet fully rigorous, level.
Original languageEnglish
Title of host publicationDiagrammatic Representation and Inference
Subtitle of host publication7th International Conference, Diagrams 2012, Canterbury, UK, July 2-6, 2012. Proceedings
EditorsPhilip Cox, Beryl Plimmer, Peter Rodgers
PublisherSpringer-Verlag GmbH
Number of pages15
ISBN (Electronic)978-3-642-31223-6
ISBN (Print)978-3-642-31222-9
Publication statusPublished - 2012

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'Diagrammatically-Driven Formal Verification of Web-Services Composition'. Together they form a unique fingerprint.

Cite this