Symbolic Choreography Analysis (SChorA)


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, you can:

  • either install it using docker
    docker run --rm -itp 8080:80 nhnghia/schora

    , then open your Web browser and go to the address: http://localhost:8080

  • or follow this instruction to install it.

Its source code is freely available under GPL 2.0 here:

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.



Last modified: Oct 12, 2018