中文会议： 计算机科学

会议日期： 2006-11-01

会议地点： 广州

主办单位： 中国计算机学会

作　　者： ; ; ;

机构地区： 中山大学信息科学与技术学院计算机科学系

出　　处： 《第二十三届中国数据库学术会议(NDBC2006)》

摘　　要： 一个工作流模型,其正确性、有效性以及性能效率等都是受人关注的.一个包含错误的工作流过程定义有可能会导致顾客的不满、处理出错等一系列问题;而定义的瑕疵则可能会引发服务效率低、存储容量超额等.所以,在工作流模型投入使用之前,对其定义进行分析是必须的.通常,把对工作流过程定义的分析划分成两种:一种是分析模型能否达到预设的性能要求;另外一种是验证模型是否满足需求,流程定义是否正确.前者一般通过系统仿真技术得到各项指标的估算值;而后者则有覆盖图、模型检测、约简等相关分析技术,这些方法要求用户具备较深入的理论知识.本文将介绍使用模型检测工具Spin对工作流进行性质验证,构造一个简单而方便的工作流模型验证环境,以提高该项工作的易用性. 由于工作流模型的建模者通常都是由熟悉业务流程的行业经理完成,而工作流的性质验证则是一项相对他们来说比较困难的工作.本文提出了使用模型检测工具Spin来对工作流模型进行性质验证,提出了工作流模型到Spin输入语言Promela的转换规则,构造了一个模型性质验证的自动化环境,方便建模者进行模型性质分析验证.由于Spin目前只能支持不带时间的模型性质验证,但由于时间是工作流模型中一个重要的影响因子,对赋时工作流模型进行验证是本文的进一步工作。

关 键 词： 工作流模型 模型检测 覆盖图 属性约简

领　　域： [自动化与计算机技术]