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.
|Title of host publication||Diagrammatic Representation and Inference|
|Subtitle of host publication||7th International Conference, Diagrams 2012, Canterbury, UK, July 2-6, 2012. Proceedings|
|Editors||Philip Cox, Beryl Plimmer, Peter Rodgers|
|Number of pages||15|
|Publication status||Published - 2012|
|Name||Lecture Notes in Computer Science|
|Publisher||Springer Berlin / Heidelberg|