Abstract: Aiming at the problem that Business Process Modeling Notation(BPMN) does not allow for formal analysis, this paper proposes a method to describe BPMN choreography pattern by Pi-calculus to realize describing BPMN choreography. BPMN choreography pattern is service interaction pattern in BPMN. Experimental result shows that this method can find and eliminate the deadlock of BPMN choreography.

Key words: Business Process Modeling Notation(BPMN), Pi-calculus, choreography

摘要： 针对业务流程建模标记(BPMN)无法依靠自身对编排进行形式化分析的问题，提出用Pi演算描述BPMN编排模式，实现对BPMN编排的描述。BPMN编排模式是服务交互模式的BPMN表达。实验结果表明，该方法能够找到并排除BPMN编排中的死锁。

关键词: 业务流程建模标记, Pi演算, 编排

CLC Number: 

• TP393