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

Business process modeling and formal verification

作　　者：吴明晖[1,2] 应晶[1,2] 

机构地区：[1]浙江大学城市学院计算机科学与工程学系,浙江杭州310015 [2]浙江大学计算机科学与技术学院,浙江杭州310027

出　　处：《浙江大学学报（工学版）》2011年第2期280-287,共8页Journal of Zhejiang University：Engineering Science

基　　金：国家863高技术研究发展计划项目(2007AA01Z187)

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

关 键 词：过程模型 环境本体 模型求精 形式化验证 ALLOY 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]