Please wait a minute...
浙江大学学报(工学版)
J4  2011, Vol. 45 Issue (2): 280-287    DOI: 10.3785/j.issn.1008-973X.2011.02.014
    
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
Download:   PDF(0KB) HTML
Export: BibTeX | EndNote (RIS)      

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.

Published: 17 March 2011
CLC:  TP 311  
Service
E-mail this article
Add to my bookshelf
Add to citation manager
E-mail Alert
RSS
Articles by authors
Cite this article:

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

URL:

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


业务过程建模及其形式化验证

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

［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] KE Hai-feng, YING Jing. Real-time license character recognition technology based on R-ELM[J]. J4, 2014, 48(2): 0-0.
[2] JIN Cang-hong, WU Ming-hui, YING Jing. A context-aware index based text extraction framework[J]. J4, 2013, 47(9): 1537-1546.
[3] ZHU Fan-wei, WU Ming-hui, YING Jing. Faceted Web search approach for large scale unstructured data[J]. J4, 2013, 47(6): 990-999.
[4] FENG Pei-en, LIU Yu, QIU Qing-ying, LI Li-xin. Strategies of efficiency improvement for Eclat algorithm[J]. J4, 2013, 47(2): 223-230.
[5] LIU Ying, CHEN Ling, CHEN Gen-cai, ZHAO Jiang-qi, WANG Jing-chang. Approach for collection selection based on click-through data[J]. J4, 2013, 47(1): 23-28.
[6] YIN Ting, XIAO Min, CHEN Ling, ZHAO Jiang-qi, WANG Jing-chang. CQPM based OLAP query log mining and recommendation[J]. J4, 2012, 46(11): 2052-2060.
[7] XIAO Min, CHEN Iing, XIA Hai-yuan, CHEN Gen-cai. Data warehouse native feature based OLAP querying with keywords[J]. J4, 2012, 46(6): 974-979.
[8] ZHANG Li-ping, LI Song, HAO Xiao-hong, HAO Zhong-xiao. Jrv  rough Vague region relation[J]. J4, 2012, 46(1): 105-111.
[9] CHEN Ling, XU Xiao-long, YANG Qing, CHEN Gen-cai. Wireless signal strength propagation model
 base on cubic spline interpolation[J]. J4, 2011, 45(9): 1521-1527.
[10] FU Chao-yang, GAO Ji, ZHOU You-ming. Service discovery based on integrating lexical multi-level hashing
with subsumption semantics[J]. J4, 2010, 44(12): 2274-2283.
[11] YANG Qing, CHEN Ling, CHEN Gen-Cai. Estimating walking distance based on single accelerometer[J]. J4, 2010, 44(9): 1681-1686.
[12] XIONG Wei, WANG Xiao-Tun. Method for mapping software dependability requirements
based on quality function deployment[J]. J4, 2010, 44(5): 881-886.
[13] ZHANG Yin, HE Gao, DIAO Li-Na, ZHANG San-Yuan. Abstract state machine design of Internetware model[J]. J4, 2010, 44(5): 923-929.
[14] JIANG Chao, YING Jing, TUN Meng-Hui, et al. Feature increment oriented  approach for software product line analysis[J]. J4, 2009, 43(12): 2142-2148.
[15] CHEN Bin, TAO Min. Mining associated and item-item correlated frequent patterns[J]. J4, 2009, 43(12): 2171-2177.