Marco Carbone (IT University of Copenhagen) |
Davide Grohmann (IT University of Copenhagen) |
Thomas T. Hildebrandt (IT University of Copenhagen) |
Hugo A. López (IT University of Copenhagen) |
We explore logical reasoning for the global calculus, a coordination model based on the notion of choreography, with the aim to provide a methodology for specification and verification of structured communications. Starting with an extension of Hennessy-Milner logic, we present the global logic (GL), a modal logic describing possible interactions among participants in a choreography. We illustrate its use by giving examples of properties on service specifications. Finally, we show that, despite GL is undecidable, there is a significant decidable fragment which we provide with a sound and complete proof system for checking validity of formulae. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.69.3 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |