Choreography modelling based on π calculus

Jiulei Jiang, Jiao Zhang, Wenxing Bao

COMPUTER MODELLING & NEW TECHNOLOGIES 2014 18(12C) 187-194

College of Computer Science and Engineering, Beifang University of Nationalities, 750021, Yinchuan, China

Business process modelling is a key step in business process management, and it plays a crucial role in process analysis and optimization. When modelling complex business process interaction, the original BPMN modelling approach is not applicable, need special modelling language and methodology for process choreography. In order to solve semantic ambiguity and integrity of business process modelling, proposed a formalize business process choreography modelling method based on π calculus. First business process choreography graphical instance design is presented by BPMN2.0 choreography. Then formal definition based on π calculus of BPMN2.0 choreography's basic activities and structured activities is presented. Then an instance of business process choreography auction scene model is given, and the model is analysed and validated manually and automatically respectively. Finally, we propose a π calculus model validation algorithm with the model XML document of Visio BPMN2.0 Modeller tool as input and then implement the algorithm. Theoretical analysis and experimental results show that this method can describe BPMN choreography by π calculus and be able to validate the semantic error of BPMN in terms of translate semantics and automatic deductive of π calculus, which makes choreography modelling more precise and specification.