Analyzing Realizability of BPMN Choreographies

BPMN choreographies specify a global message order of systems, which enables to build systems by composing a set of interacting peers that communicate with each via exchanging messages. Analyzing the realizability of choreographies is a crucial problem in top-down development. In this paper, we present an approach for analyzing the realizability of choreographies for both synchronous and asynchronous communication, which allows us to 1) encode a choreography into CSP# processes for generating the choreography LTS under the tool support, 2) automatically obtain peers from the generated choreography LTS, 3) check whether the choreography specification is realizable for both synchronous communication and asynchronous communication, where behavior equivalence checking is used to compare the choreography LTS with the LTS of the distributed system that is composed of the generated peers. Finally, experimental results show that our approach is effective.