VerChor: A Framework for the Design and Verification of Choreographies

Matthias Güdemann 1 Pascal Poizat 2, 3 Gwen Salaün 1 Lina Ye 1
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
3 MoVe - Modélisation et Vérification
LIP6 - Laboratoire d'Informatique de Paris 6
Abstract : Choreographies are contracts specifying from a global point of view the legal interactions that must take place among a set of services. Such a contract may serve as a reference in the development of concurrent distributed system, whether it is achieved following a top-down or a bottom-up approach. In this article, we present VerChor, a generic, modular, and extensible framework for supporting the development based on choreographies. It relies on a choreography intermediate format (CIF) into which several existing choreography description languages can be transformed. VerChor builds around a set of formal properties whose verification is central to choreography-based development. To support this development process, we propose a connection between CIF and the CADP verification toolbox, which enables the full automation of the aforementioned properties. Finally, we illustrate a practical use of the VerChor framework through its integration with the Eclipse BPMN 2.0 designer.
Document type :
Journal articles
IEEE Transactions on Services Computing, IEEE, 2016, 9 (4), pp.647-660. 〈10.1109/TSC.2015.2413401〉
Liste complète des métadonnées

Cited literature [43 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-01198918
Contributor : Lip6 Publications <>
Submitted on : Monday, March 21, 2016 - 10:42:21 AM
Last modification on : Friday, March 17, 2017 - 10:49:27 AM
Document(s) archivé(s) le : Wednesday, June 22, 2016 - 10:43:12 AM

File

TSC-2013-12-0224-author.pdf
Files produced by the author(s)

Identifiers

Citation

Matthias Güdemann, Pascal Poizat, Gwen Salaün, Lina Ye. VerChor: A Framework for the Design and Verification of Choreographies. IEEE Transactions on Services Computing, IEEE, 2016, 9 (4), pp.647-660. 〈10.1109/TSC.2015.2413401〉. 〈hal-01198918〉

Share

Metrics

Record views

561

Document downloads

206