Analyzing Chor Specifications by Translation into FSP

AbstractA choreography specifies activities and interactions among a set of services from a global point of view. From this specification, local implementations or peers can be automatically generated. Generation of peers that precisely implement the choreography specification is not always possible: this problem is known as realizability. This paper presents an encoding of the Chor choreography calculus into the FSP process algebra. This encoding allows to: (i) validate and verify Chor specifications using the FSP toolbox (LTSA), (ii) generate peer protocols from its choreography specified in Chor, (iii) test for realizability of the Chor specification, and (iv) generate Java code from FSP for rapid prototyping purposes. Our proposal is supported and completely automated by a prototype tool we have implemented