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.