Abstract
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.
Original language | English |
---|---|
Journal | Places |
Volume | 69 |
Pages (from-to) | 29-43 |
ISSN | 0731-0455 |
Publication status | Published - 2010 |
Keywords
- Choreography
- Specifications
- Modal Logic
- Undecidable
- Coordination Models
- Logical Reasoning
- Hennessy-Milner Logic
- Global Calculus
- Proof Systems