| BPMN 2.0编排的形式语义和分析 |
| |
| 引用本文： | 代飞,赵文卓,杨云,莫启,李彤,周华.BPMN 2.0编排的形式语义和分析[J].软件学报,2018,29(4):1094-1114. |
| |
| 作者姓名： | 代飞 赵文卓 杨云 莫启 李彤 周华 |
| |
| 作者单位： | 西南林业大学 计算机与信息学院, 云南 昆明 650091;云南大学 软件学院, 云南 昆明 650091;云南省软件工程重点实验室, 云南 昆明 650091,云南大学 软件学院, 云南 昆明 650091,云南大学 软件学院, 云南 昆明 650091;云南省软件工程重点实验室, 云南 昆明 650091,云南大学 软件学院, 云南 昆明 650091;云南省软件工程重点实验室, 云南 昆明 650091,云南大学 软件学院, 云南 昆明 650091;云南省软件工程重点实验室, 云南 昆明 650091,西南林业大学 计算机与信息学院, 云南 昆明 650091 |
| |
| 基金项目： | 国家自然科学基金资助项目（61462095，61663046，61402397，61379032）；云南省自然科学基金资助项目（2016FB102，2016FB104），云南省中青年学术和技术带头人后备人才培养项目（C6143002），云南省软件工程重点实验室开放基金面上项目（2017SE201，2016SE202，2015SE102），云南省教育厅科学研究基金重大专项项目（ZD2014001） |
| |
| 摘 要： | BPMN 2.0编排已成为描述业务流程间交互事实上的标准.BPMN 2.0编排面向流的特征，使之会产生控制流方面的语义错误.因此，检查编排语义正确性是BPMN 2.0编排建模工具所期望具有的功能.但是，BPMN 2.0标准规约中编排缺少形式语义及相应的分析技术，这阻碍了对BPMN 2.0编排的语义分析.本文提出了一种映射，用于将BPMN 2.0编排转换为工作流网，使用Petri网来形式定义BPMN 2.0编排的语义.借助Petri网的分析技术，这种定义的语义可用来分析BPMN 2.0编排的结构和控制流方面的错误.该映射和语义分析已被实现为一种工具.实验结果表明，这种形式化可以识别BPM AI过程模型库中编排的语义错误.
|
| 关 键 词： | 业务流程建模标注2.0 编排 Petri网 形式语义 语义分析 |
| 收稿时间： | 2016/10/5 0:00:00 |
| 修稿时间： | 2016/11/25 0:00:00 |
Formal Semantics and Analysis of BPMN 2.0 Choreographies |
| |
| DAI Fei,ZHAO Wen-Zhuo,YANG Yun,MO Qi,LI Tong and ZHOU Hua.Formal Semantics and Analysis of BPMN 2.0 Choreographies[J].Journal of Software,2018,29(4):1094-1114. |
| |
| Authors: | DAI Fei ZHAO Wen-Zhuo YANG Yun MO Qi LI Tong and ZHOU Hua |
| |
| Affiliation: | Computer and information technology College, Southwest Forestry University, Kunming 650091, China;School of Software, Yunnan University, Kunming 650091, China;Key Laboratory for Software Engineering of Yunnan Province, Kunming 650091, China,School of Software, Yunnan University, Kunming 650091, China,School of Software, Yunnan University, Kunming 650091, China;Key Laboratory for Software Engineering of Yunnan Province, Kunming 650091, China,School of Software, Yunnan University, Kunming 650091, China;Key Laboratory for Software Engineering of Yunnan Province, Kunming 650091, China,School of Software, Yunnan University, Kunming 650091, China;Key Laboratory for Software Engineering of Yunnan Province, Kunming 650091, China and Computer and information technology College, Southwest Forestry University, Kunming 650091, China |
| |
| Abstract: | The Business Process Modelling Notation 2.0 (BPMN 2.0) choreography is a de factor standard for capturing the interactions between business processes. Flow-oriented BPMN 2.0 choreographies can exhibit a range of semantic errors in the control flow. The ability to check the semantic correctness of choreographies is thus a desirable feature for modelling tools based on BPMN 2.0 choreographies. However, the semantic analysis of BPMN 2.0 choreographies is hindered by the lack of formal semantic definition of its constructs and the corresponding analysis techniques in the BPMN 2.0 standard specification. This paper defines a formal semantics of BPMN 2.0 choreographies in terms of a mapping to WF-nets. This defined semantics can be used to analyze the structural errors and the control flow errors of BPMN 2.0 choreographies, using analysis techniques of Petri nets. The proposed mapping and the semantic analysis have been implemented as a tool. The experimental results show this formalization can identify the semantic errors of choreographies from the BPM AI process model library. |
| |
| Keywords: | Business Process Modeling Notation 2 0 Choreography Petri Nets Formal Semantics Semantics Analysis |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
