Symbolic Choreography Analysis (SChorA)

Overview

Choreography is the description with a global perspective of interactions between roles played by peers (services, organizations, humans) in some collaboration. A choreography has two components: a set of roles, and the specification of the legal orderings of message exchanges between these roles. The key issue in choreography-based top-down development is:

  • Conformance: Does a set of peers conform to the choreography? (each peer plays a role and the interactions between them respect to the choreography specification)
  • Realizability: Whether a choreography is realizable? (is there a such set of peers which conform to the choreography? If yes, how to get them or their models?)

Some challenges:

  • Lack of formal model of choreography with value-passing
  • State space explosion problem when checking/analyzing choreographies

SChorA framework

SChorA addresses these issues with symbolic approach. The value-passings are reasoned by using symbols rather than their concrete values. Conclusion is given thank to SMT solver.

Principal features of SChorA:

  • Check whether two models are conform (using branching bi-simulation)
  • Retire role models from a choreography
  • Get the reachable model of a choreography
  • Get a realizable model of a choreography
  • Product local models
  • Represent graphically a model

You can try SChorA directly from web browsers. No configs are required (tested with Safari 6.02, Firefox 16.02, Chrome 25.0.1364.99, and Opera 12.04)

If you want to use SChorA on local machine, please follow this instruction to install it.

Its source code is freely available under GPL 2.0 here: https://github.com/nhnghia/schora

SChorA syntax

A SChorA script file consists of two parts: declaration and command. In the declaration part, the models of choreography, role, or peer are declared in component and end component. The command part describes commands to manipulate models above, e.g., conformance A B to check whether A conforms to B.

For further information of syntax, go here.

Publications

Contact

Last modified: December 19, 2014