VerChor: A Framework for Verifying Choreographies

Matthias Güdemann 1 Pascal Poizat 2, 3 Gwen Salaün 1, * Alexandre Dumont 1
* Auteur correspondant
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
2 MoVe - Modélisation et Vérification
LIP6 - Laboratoire d'Informatique de Paris 6
Abstract : Choreographies are contracts specifying interactions among a set of services from a global point of view. These contracts serve as reference for the further development steps of the distributed system. Therefore their specification and analysis is crucial to avoid issues (e.g., deadlock, requirement violation, faulty contract, etc.) that may induce delays and additional costs if identified lately in the design and development process. In this paper, we propose first to describe choreographies using an intermediate format in order to support various choreography specification languages as input. Second, we propose a connection to a formal verification toolbox as back-end, which includes the generation of verification scripts for fully automating the aforementioned checks. This results in a generic, modular, and extensible framework for supporting the verification of choreographies.
Type de document :
Communication dans un congrès
Fundamental Approaches to Software Engineering 2013, Mar 2013, Rome, Italy. 7793, pp.226-230, 2013, Lecture Note in Computer Science. 〈10.1007/978-3-642-37057-1_16〉
Liste complète des métadonnées

Littérature citée [6 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00806788
Contributeur : Gwen Salaün <>
Soumis le : mardi 2 avril 2013 - 13:07:33
Dernière modification le : mardi 13 décembre 2016 - 15:45:50
Document(s) archivé(s) le : mercredi 3 juillet 2013 - 04:06:52

Fichier

main-fase13.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Matthias Güdemann, Pascal Poizat, Gwen Salaün, Alexandre Dumont. VerChor: A Framework for Verifying Choreographies. Fundamental Approaches to Software Engineering 2013, Mar 2013, Rome, Italy. 7793, pp.226-230, 2013, Lecture Note in Computer Science. 〈10.1007/978-3-642-37057-1_16〉. 〈hal-00806788〉

Partager

Métriques

Consultations de
la notice

441

Téléchargements du document

177