Howto: Conformance Checking

This page presents how to use SChorA to check the conformance of a choreography implementation impl and a choreography specification spec.

  • If you know the models of impl and spec, then follow the first section
  • If you know the model of spec and n local models of peers participating in the implementation impl then follow the second section.

Check "impl conforms to spec"

  1. goto SChorA IDE: http://schora.lri.fr/ide
  2. click on New button to create a new SChorA script
  3. enter the models of impl and spec after DECLARATIONS keyword. Each model is put into component and end component keywords. For example:
    DECLARATIONS
        component impl chorD
            request[a,b] ; response[b,a]
        end component
        component spec chorD
            request[a,b] ; response[b,a]
        end component
  4. enter a command to check conformance of impl and spec after COMMANDS keyword. For example
    COMMANDS
        conformance impl spec
  5. click on button Run to execute the script
  6. the result is display on Output tab.

Check "a set of local peers conforms to spec"

This checking is realized as the section above, except the step 3 in which, you declare the models of local peers and the one of spec, and the composition of these local peers. Particularly, each declaration is put into component and end component keywords. The composition is also put into these keywords. For example:

DECLARATIONS
    component peer1 chorD
        request[a,b]! ; response[b,a]?
    end component
    component peer2 chorD
        request[a,b]? ; response[b,a]!
    end component
    //composition
    component impl chorD
        peer1 || peer2
    end component

This example describes 3 components: the two first components presents two peers, the last one is the composition of these peers.

Last modified: July 11, 2013