VerChor Framework

VerChor enables you to design correct distributed systems following the choreography-based development approach. Just model the system interaction protocol in your favorite language and let VerChor check for its realizability and retrieve peer interaction skeletons, or let it generate peer controllers to ensure the conformance to the system specification of a set of peers you want to reuse !

Matthias Güdemann, Pascal Poizat, Gwen Salaün, and Lina Ye. VerChor: A Framework for the Design and Verification of Choreographies. IEEE Transactions on Services Computing, 9(4) :647-660, 2016. [DOI] [HAL Open Archive]

Click-and-play choreography verification

Verification is often found to be a tedious and complex task. Through integration with the Eclipse IDE and its choreograpy modeling plugins, formal models and verification algorithms are transparent to you if you want so. Just select the analysis you want to perform on the choreography model you are designing and let VerChor do all the work !

Feedback for choreography fixing

Formal verification results are often disconnected from the model they apply to. With VerChor, the outcomes of choreography analysis are presented directly in the choreography modeler. Precise diagnosis information helps you fixing badly-formed choreographies.

Comprehensive analysis techniques

For bottom-up development VerChor includes checking whether a set of peer models are conform to a choreography specification, and for top-down development it enables checking whether a choreography can be correctly implemented as a distributed system (under different communication semantics) and generating peer interaction skeletons.

Model-driven formal engineering

VerChor follows a model-driven approach to the choreography-based engineering of distributed systems. Front-ends transform choreographies written in high-level description languages into the CIF pivot model. Back-ends transform CIF models into formal models and perform analyses using dedicated top-notch formal verification tools.

Supported languages and notations

Front-ends: VerChor supports choreography description using the ISO standard BPMN 2.0 notation.
Back-ends: VerChor supports verification using the LOTOS NT formal notation and the CADP state-of-the-art verification tool.

Open source collaborative framework

The VerChor Framework is licensed under the GNU GPL v2.0 license. Join us to develop a front-end for your favorite choreography modeling language or to extend analysis features using new algorithms, new formal models, or new verification tools.