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 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: https://github.com/nhnghia/schora

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.

• Huu Nghia Nguyen. A Symbolic Approach for the Verification and the Test of Service Choreographies. PhD thesis, under the supervision of Pascal Poizat and Fatiha Zaïdi. October 2013.
• Huu Nghia Nguyen, Pascal Poizat and Fatiha Zaïdi. Automatic Skeleton Generation for Data-Aware Service Choreographies. in ISSRE'2013 - IEEE International Symposium on Software Reliability Engineering. November 2013.
• Huu Nghia Nguyen, Pascal Poizat and Fatiha Zaïdi. A Symbolic Framework for the Conformance Checking of Value-Passing Choreographies. in ICSOC'2012 - International Conference on Service Oriented Computing. November 2012.

• Huu Nghia NGUYEN
• Pascal POIZAT
• Fatiha ZAÏDI

Last modified: Oct 12, 2018