Abstract
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. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Papapanagiotou, P., Fleuriot, J., & Wilson, S. (2012). Diagrammatically-driven formal verification of web-services composition. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7352 LNAI, pp. 241–255). https://doi.org/10.1007/978-3-642-31223-6_25
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
