Please wait a minute...
浙江大学学报(工学版)
J4  2011, Vol. 45 Issue (2): 280-287    DOI: 10.3785/j.issn.1008-973X.2011.02.014
计算机技术     
业务过程建模及其形式化验证
吴明晖1,2, 应晶1,2
1. 浙江大学城市学院 计算机科学与工程学系,浙江 杭州 310015；
2. 浙江大学 计算机科学与技术学院,浙江 杭州 310027
Business process modeling and formal verification
WU Ming-hui1,2, YING Jing1,2
1. Department of Computer Science and Engineering, Zhejiang University City College, Hangzhou 310015, China；
2. College of Computer Science and Technology, Zhejiang University, Hangzhou 310027, China
 全文: PDF  HTML
摘要：

针对业务过程建模复杂、模型一致性难以保证的问题,提出一种求精式业务过程建模及其形式化验证方法.结合语义本体技术、基于统一建模语言(UML)的扩展机制,实现对业务过程中的不同关注点进行多视角地可视化建模.业务过程建模是一个“整体抽象过程→声明式过程→命令式过程”多阶段的求精过程.引入环境本体的概念,以软件交互对环境状态的影响来描述软件行为和能力,并在此基础上给出了模型相关定义及其形式化语义.结合一个简化的产品交易系统实例详细论述如何采用声明式形式化语言Alloy进行业务过程模型定义和模型求精的形式化验证.实例表明,采用分阶段求精式业务过程建模方法,并围绕模型语义通过Alloy语言进行形式化验证,可以有效地提升建模过程的灵活性和保证模型规范的一致性.
Abstract:

Business process is with high complexity, and it is hard to keep the models consistent. In order to deal with the problem, an approach for business process modeling and formal verification was proposed. Combing with semantic ontology technology, based on unified modeling language (UML) extensions, the approach supports visual modeling with multiple views according to different concerns in business process. The business modeling consists of three stages of refinements: 1) whole abstract process; 2) declarative process; 3) imperative process. By adopting the concept of “environment ontology”, the capabilities and behaviors of software can be specified by the effects of changing environment status. Based on the idea, the modeling related definitions and their formal semantics are presented. At last, an example of simplified products trading system demonstrates how to verify process model definition and model refinement specification with Alloy in details. The example shows that modeling business process approach and verifying the model specifications with Alloy can improve the model process flexibility and ensure models consistency.
出版日期: 2011-03-17
:  TP 311  
基金资助:

国家863高技术研究发展计划项目(2007AA01Z187).
通讯作者: 应晶,（1971—）,男,教授,博导.     E-mail: yingj@zucc.edu.cn
作者简介: 吴明晖,（1976—）,男,江西南昌人,副教授,博士生,从事软件工程和服务工程研究.E-mail: minghuiwu@cs.zju.edu.cn
服务　　
把本文推荐给朋友
加入引用管理器
E-mail Alert
RSS
作者相关文章　　

引用本文:

吴明晖, 应晶. 业务过程建模及其形式化验证[J]. J4, 2011, 45(2): 280-287.

WU Ming-hui, YING Jing. Business process modeling and formal verification. J4, 2011, 45(2): 280-287.

链接本文:

http://www.zjujournals.com/eng/CN/10.3785/j.issn.1008-973X.2011.02.014    或    http://www.zjujournals.com/eng/CN/Y2011/V45/I2/280

［1］ OMG Document Number: formal/2011-01-03, Business process modeling and notation (BPMN) (version 2.0) ［S］, Needham, USA: Object Management Group, 2011.
［2］ EVANS A, FRANCE R, GRANT E. Towards formal reasoning with UML models ［C］∥ Proceedings of the ObjectOriented Programming, Systems, Languages, and Applications Workshop on Behavioral Semantics. Denver, USA: Springer, 1999: 67-73.
［3］ MARCANO R, LEVY N. Using B formal specifications for analysis and verification of UML/OCL models ［C］ ∥Proceedings of the Workshop on Consistency Problems in UMLBased Software Development. 5th International Conference on the Unified Modeling Language. Dresden, Germany: Springer, 2002: 97-111.
\
[4\] ANASTASAKIS K, BORDBAR B, GEORG G, et al. UML2Alloy: a challenging model transformation \
[C\] ∥Proceedings of the ACM/IEEE 10th International Conference on Model Driven Engineering Languages and Systems. Nashville, Tennessee: Springer, 2007: 436-450.
［5］ RYCHKOVA I, REGEY G, WEGMANN A. Using declarative specifications in business process design ［J］. International Journal of Computer Science and Applications, 2008, 5(3b): 45-68.
［6］ WU Minghui, YING Jing, YAN Hui. Semantic model driven architecture based method for enterprise application development ［C］∥ Proceedings of the 2009 International Conference on Web Information Systems and Mining. Shanghai: Springer, 2009: 299-308.
［7］ 吕瑞峰,王刚,问晓先等,基于模型驱动框架的计算无关层过程建模［J］.计算机集成制造系统,2008, 14(5): 868-874.
LV Ruifeng, WANG Gang, WEN Xiaoxian, et al. Process modeling method of calculation independent model level based on M DA ［J］. Computer Integrated Manufacturing Systems. 2008, 14(5): 868-874.
［8］ 吴步丹,金芝,赵彬,面向服务的建模：一种全过程复用的方法［J］.计算机学报,2008,31(8): 1293-1307
WU Budan, JIN Zhi, ZHAO Bin, et al. Serviceoriented modeling based on whole process asset reuse ［J］. Chinese Journal of Computers. 2008, 31(8): 1293-1307.
［9］ JACKSON D. Software abstractions: logic, language, and analysis ［M］. Cambridge, Massachusetts: MIT Press. 2006: 253-290.
［10］ BORDBAR B, ANASTASAKIS K. UML2Alloy: A tool for lightweight modelling of discrete event systems ［C］∥Proceedings of the IADIS International Conference in Applied Computing 2005. Algarve, Portugal: IADIS Press, 2005: 209-216.
[1] 柯海丰,应晶. 基于R-ELM的实时车牌字符识别技术[J]. J4, 2014, 48(2): 0-0.
[2] 金苍宏,吴明晖,应晶. 一种基于上下文索引的文本匹配框架[J]. J4, 2013, 47(9): 1537-1546.
[3] 朱凡微, 吴明晖, 应晶. 面向大规模无结构数据的Web方面搜索方法[J]. J4, 2013, 47(6): 990-999.
[4] 冯培恩, 刘屿, 邱清盈, 李立新. 提高Eclat算法效率的策略[J]. J4, 2013, 47(2): 223-230.
[5] 刘颖, 陈岭, 陈根才, 赵江奇, 王敬昌. 基于历史点击数据的集合选择方法[J]. J4, 2013, 47(1): 23-28.
[6] 殷婷,肖敏,陈岭,赵江奇,王敬昌. 基于CQPM的OLAP查询日志挖掘及推荐[J]. J4, 2012, 46(11): 2052-2060.
[7] 肖敏, 陈岭, 夏海元, 陈根才. 基于数据仓库内在特征的OLAP关键词查询[J]. J4, 2012, 46(6): 974-979.
[8] 张丽平,李松,郝晓红,郝忠孝. Jrv粗糙Vague区域关系[J]. J4, 2012, 46(1): 105-111.
[9] 陈岭,许晓龙,杨清,陈根才. 基于三次样条插值的无线信号强度衰减模型[J]. J4, 2011, 45(9): 1521-1527.
[10] 傅朝阳, 高济, 周尤明. 词法多重散列与包容语义相结合的服务查找[J]. J4, 2010, 44(12): 2274-2283.
[11] 杨清, 陈岭, 陈根才. 基于单加速度传感器的行走距离估计[J]. J4, 2010, 44(9): 1681-1686.
[12] 熊伟, 王晓暾. 基于质量功能展开的可信软件需求映射方法[J]. J4, 2010, 44(5): 881-886.
[13] 张引, 何浩, 赵丽娜, 张三元. 网构软件模型中的抽象状态机设计[J]. J4, 2010, 44(5): 923-929.
[14] 蒋涛, 应晶, 吴明晖, 等. 一种面向特征增量的软件产品线分析方法[J]. J4, 2009, 43(12): 2142-2148.
[15] 沈斌, 姚敏. 关联且项项正相关频繁模式挖掘[J]. J4, 2009, 43(12): 2171-2177.