Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
Diagrammatically-Driven Formal Verification of Web-Services Composition
verfasst von : Petros Papapanagiotou, Jacques Fleuriot, Sean Wilson
Erschienen in: Diagrammatic Representation and Inference
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.