基于UML的工作流模型自动分析验证研究-计算机软件与理论专业论文.docx
文本预览下载声明
摘
摘 要
工作流是在计算机辅助下全部或部分自动执行的工作过程。Internet的发展 对工作流的发展起了极大的促进作用,使计算机支持的分布式、协同工作的工作 流系统在企、事业单位中得到越来越多的应用。在现实世界中设计一个应用工作 流是一个复杂而易出错的过程。缺少有效的方法和工具保证工作流的『F确性已成 为工作流得到进一步广泛应用的一个障碍。
模型检测(Model Checking)是一种采用形式化方法的自动分析和验证技术, 相对于传统形式化证明方法,具有快速、准确、全自动、对使用人员数学背景要 求不高的特点,目前已在协议验证、分布式系统的设计和验证等方面得到成功的 应用,为工作流模型验证提供了新的方法。
本论文研究使用模型检测技术的工作流模型的验证方法。沦文首先介绍了工 作流相关概念以及模型检测技术的理论和方法,其中对模型检测工具Spin及其 输入语言作了较详细的阐述。然后对工作流模型及其UML建模方法进行研究, 提出基于UML的以模型检测为目的的工作流模型建模方法,并定义了模型的形 式化描述;定义了工作流的形式化模型到Spin/Promela模型的转化规则,使用 Spin对工作流模型的结构、语义正确性进行分析和验证。在前面工作的基础上设 计了一个基于UML的工作流模型的自动分析和验证的工具,实现由工作流UML 模型到Spin/Promela模型的自动转化,使不熟悉模型检测技术的工作者也能使用
该方法对工作流进行验证。
关键字:工作流:UML;模型检测;Spin
第1负
Abstract
Abstract
Workflow is business process executing completely partially automatically with the aid of computer.The development of Intemet has greatly promoted the development of workflow in the past twenty years.Computer supported cooperation
and distributed workflow systems becoming more and more widely used in governments and enterprises.Yet in realistic world,designing application workflow is complex and fallible process.Lack of effective means and tools has been of the obstacles for workflow be further and more widely used.
Model Checking is an automatic analysis and verification technology using formal methods.Compared with traditional formal methods,it is fast,completely automatic and does require strong mathematic background.Presently model checking has been successfully applied in several fields such protocol verification,
design and verification of distributed system.It provides new method for workflow
verification.
This paper focuses the verification methods of workflow model based model checking.It firstly introduces relative conceptions about workflow and the theories and methods of model checking,mainly describing the work of model checking tool Spin and its model language Promela.Based the study of the character of workflow model and modelling methods using UML,it puts forward
modelling method especially aimin
显示全部