（计算机软件与理论专业论文）基于uml的工作流模型自动分析验证研究.pdf

华南师范大学硕士学位论文答辩合格证明 学位申请人塑遨盏 向本学位论文答辩委员会提交 题为妻童幽圭垡圣堡盘盔鲤鱼亟筮堑量蛀壬邈亟的硕士论文， 经答辩委员会审议，本论文答辩合格，特此证明。 学位论文答辩委员会委员( 签名) 主席：鲍改 豫避吻 色， 论文指导老师( 签名) ： b r a b 摘要 工作流是在计算机辅助下全部或部分自动执行的工作过程。i n t e r n e t 的发展 对工作流的发展起了极大的促进作用，使计算机支持的分布式、协同工作的工作 流系统在企、事业单位中得到越来越多的应用。在现实世界中设计一个应用工作 流是一个复杂而易出错的过程。缺少有效的方法和工具保证工作流的f 确性已成 为工作流得到进一步广泛应用的一个障碍。 模型检测( m o d e lc h e c k i n g ) 是一种采用形式化方法的自动分析和验证技术， 相对于传统形式化证明方法，具有快速、准确、全自动、对使用人员数学背景要 求不高的特点，目前已在协议验证、分布式系统的设计和验证等方面得到成功的 应用，为工作流模型验证提供了新的方法。 本论文研究使用模型检测技术的工作流模型的验证方法。沦文首先介绍了工 作流相关概念以及模型检测技术的理论和方法，其中对模型检测工具s p i n 及其 输入语言作了较详细的阐述。然后对工作流模型及其u m l 建模方法进行研究， 提出基于u m l 的以模型检测为目的的工作流模型建模方法，并定义了模型的形 式化描述；定义了工作流的形式化模型到s p i n p r o m e l a 模型的转化规则，使用 s p i n 对工作流模型的结构、语义正确性进行分析和验证。在前面工作的基础上设 计了一个基于u m l 的工作流模型的自动分析和验证的工具，实现由工作流u m l 模型到s p i n p r o m e l a 模型的自动转化，使不熟悉模型检测技术的工作者也能使用 该方法对工作流进行验证。 关键字：工作流：u m l ；模型检测；s p i n 第1 负 a b s 仃a c l a b s t r a c t w o r k f l o wi sab u s i n e s sp r o c e s se x e c u t i n gc o m p l e t e l yo rp a r t i a l l ya u t o m a t i c a l l y w i t ht h e a i do fc o m p u t e r t h ed e v e l o p m e n to fi n t e m e th a sg r e a t l yp r o m o t e dt h e d e v e l o p m e n to fw o r k f l o wi nt h ep a s tt w e n t yy e a r s c o m p u t e rs u p p o r t e dc o o p e r a t i o n a n dd i s t r i b u t e dw o r k f l o ws y s t e m sa l eb e c o m i n gm o r ea n dm o r ew i d e l yu s e di n g o v e r n m e n t sa n de n t e r p r i s e s y e ti nr e a l i s t i cw o r l d ，d e s i g n i n ga na p p l i c a t i o n w o r k f l o wi sac o m p l e xa n df a l l i b l ep r o c e s s l a c ko fe f f e c t i v em e a n sa n dt o o l sh a s b e e noneo ft h eo b s t a c l e sf o rw o r k f l o wt ob ef u r t h e ra n dm o r ew i d e l yu s e d m o d e lc h e c k i n gi sa na u t o m a t i ca n a l y s i sa n dv e r i f i c a t i o n t e c h n o l o g yu s i n g f o r m a lm e t h o d s c o m p a r e dw i t ht r a d i t i o n a lf o r m a lm e t h o d s ，i ti sf a s t ，c o m p l e t e l y a u t o m a t i ca n dd o e sn o tr e q u i r es t r o n gm a t h e m a t i cb a c k g r o u n d p r e s e n t l ym o d e l c h e c k i n gh a sb e e ns u c c e s s f u l l ya p p l i e di ns e v e r a lf i e l d ss u c ha sp r o t o c o lv e r i f i c a t i o n ， d e s i g na n d v e r i f i c a t i o no fd i s t r i b u t e ds y s t e m i tp r o v i d e san e wm e t h o df o rw o r k f l o w v e r i f i c a t i o n t h i sp a p e rf o c u s e so nt h ev e r i f i c a t i o nm e t h o d so fw o r k f l o wm o d e lb a s e do n m o d e lc h e c k i n g i tf i r s t l yi n t r o d u c e sr e l a t i v ec o n c e p t i o n sa b o u tw o r k f l o wa n dt h e t h e o r i e sa n dm e t h o d so fm o d e lc h e c k i n g ，m a i n l yd e s c r i b i n gt h ew o r ko fm o d e l c h e c k i n gt o o ls p i na n di t sm o d e ll a n g u a g ep r o m e l a b a s e do nt h es t u d yo ft h e c h a r a c t e ro fw o r k f l o wm o d e la n dm o d e l l i n gm e t h o d su s i n gu m l ，i tp u t sf o r w a r da m o d e l l i n gm e t h o de s p e c i a l l ya i m i n ga tm o d e lc h e c k i n ga n dd e f i n i t et h ef o r m a l d e s c r i p t i o nf o rt h em o d e l a s s o c i a t e dw i t ht h el a n g u a g ep r o m e l a ，t h ep a p e rd e f i n i t ea s e r i e sr u l e sf o rt r a n s l a t i n gt h ew o r k f l o wm o d e ls p e c i f i e di nu m lt oap r o g r a m m ei n p r o m e l a ，w h i c hi st h ei n p u to fs p i n ，s oa st ou s es p i nt oc h e c kw h e t h e rt h ew o r k f l o w s a t i s f i e sa r e q u i r e dp r o p e r t y f i n a l l y , i td e s i g n sa na u t o m a t i ca n a l y s i sa n dv e r i f i c a t i o n t o o lf o rw o r k f l o wm o d e ls p e c i f i e di nu m l ，w h i c hr e a l i z e st h et r a n s l a t i o nf r o ma u m lm o d e lt oap r o m e l am o d e l ，s ot h a tt h ea p p r o a c hi sa c c e s s i b l et ot h o s ep e o p l e w h oa l en o te x p e r ti nf o r m a lm e t h o d s k e yw o r d s ：w o r k f l o w ；u m l ；m o d e lc h e c k i n g ；s p i n 第2 页 第一章绪论 第一章绪论 1 1 课题背景 工作流是在计算机辅助下全部或部分自动执行的工作过程。i n t e r n e t 的发展 对工作流的发展起了极大的促进作用，使计算机支持的分布式协同工作的工作流 系统在企、事业单位中得到越来越多的应用。实际经验表明，在现实世界中设计 一个应用工作流是一个复杂而易出错的过程。工作流设计阶段的错误将导致后期 实旌上的错误。为避免这种情况的发生，十分有必要在工作流设计阶段对其进行 分析和检验。缺少有效的方法和工具保证工作流的f 确性已成为工作流褥到进一 步广泛应用的一个障碍1 1 l 。 对工作流的分析和验证主要有两种方法。一是模拟和测试，这是同前保证软 件系统i f 确性的主要方法，也是具有验证功能的工作流管理系统主要采用的方 法。j 下如这种方法很难发现软件的全部错误一样，单靠模拟和测试同样难以保证 工作流模型的正确性。二是定理证明和演绎验证，是形式化分析方法中的一种， 它首先需要定义一定的定理和证明规则，通过推导来证明系统的所具有的性质。 这种方法的缺点是较为耗时，且仅限于专家使用。 模型检测( m o d e lc h e c k i n g ) 1 2 】是一种采用形式化方法的自动分析和验证的 技术，通过建立系统的有限模型，对这个模型的状态空间进行搜索，咀确定系统 是否满足某个期望的性质。相对于传统形式化证明方法，模型检测具有快速、全 自动、对使用人员数学背景要求不高的特点。对模型检测工具的使用者丽言，需 要做的只是把需要验证的系统转换成模型检测工具的输入语言描述的模型，启动 检测工具对某些性质进行验证。若检测出系统不能满足用户所要求的性质，则报 告错误，并给出反例，帮助用户对系统进行分析和改进。由于模型检测是一种使 用状态空问搜索的技术，状态空间爆炸是模型检测的主要问题。 s p i n ( s i m p l ep r o m e l ai n t e r p r e t e r ) 1 3 1 是贝尔实验室丌发的一种模型检验工具，用 于分布式系统如数据通信协议、分布式操作系统、数据库系统的设计和验证。它 使用p r o m e t a 语言描述被验证的系统，用线性时态逻辑来描述系统要求满足的性 质。为克服状态空间爆炸问题，s p i n 使用了很多的优化技术，是目前较成熟的模 第5 页 第一章绪论 型检测工具。目的s p i n 已经在许多分布式系统的设计和验证中得到成功的应用。 在使用模型检测验证工作流上，已有部分的研究者做了这方面的工作。文献 【5 】中提出一个基于p e t r i 网的工作流验证方法，它将工作流转换成p t 网，用现 有的一个p 厂r 分析器对其进行验证，并开发出了一个实现工具w o f l a n 。其对工作 流的分析主要集中在对控制流图结构分析，不考虑工作流中各项活动具体的语 义，只能验证固定的性质，不能随应用的不同而更改。文献【6 】基于状态图、活 动图，以及一个使用c t l ( c o m p u t a t i o n t r e e l o g i c ) 逻辑的模型检测工具建立了 一个工作流分析器。文献 7 】使用一种标记迁移系统( l a b e lt r a n s i t i o ns y s t e m ，l t s ) 对工作流进行建模，使用模型检测工具t r a c t a 对模型进行的安全性、活性进 行验证。 统一建模语言u m l 是一种描述能力强大且含义直观的可视化建模语言，将 模型检测技术与u m l 建模结合以提高模型的合理性和j f 确性是目前的一个研究 方向。文献【8 基于时间自动机理论提出了一个u m l 模型的检验方法，文献【9 】 的验证方法针对基于c o r b a 应用的u m l 模型而提出，文献f 】0 1 研究了嵌入式 系统u m l 模型的检验方法，文献【1 1 】、 1 2 1 研究了u m l 顺序图和状态图的检验 方法。 1 2 本论文主要工作和目标 保证工作流模型的合理性、正确性具有非常重要的意义。模型检测技术为工 作流模型的分析验证提供了一种新的方法，本论文的主要工作是使用模型检测工 具s p i n 对工作流模型进行自动分析检测。 在对工作流模型的描述上，p e t r i 网h j 3 是目前的主流方法，具有精确的语义， 避免了模糊性和不确定性。而在系统分析和设计阶段，用可视化的手段对目标系 统进行建模，以直观的、易于理解的图形方式刻画和描述系统具有十分重要的意 义。u m l 比p e t r i 网具有更强的直观性，基于这一点，本论文采用u m l 对工作 流进行描述。因此，本论文工作包括以下几个方面： ( 1 ) 对工作流模型的特性及其u m l 建模方法进行研究，结合模型检测技 术，提出基于u m l 的适用于模型检测的工作流模型建模方法，并定义模型的形 式化描述； 第6 页 第一章绪论 ( 2 ) 对s p i n 检测理论、实现及应用进行研究，结合工具输入语言p r o m e l a ， 提出u m l 工作流的形式化模型到s p i n p r o m e l a 模型的转化，对工作流模型结构、 语义进行验证： ( 3 ) 设计一个基于u m l 的工作流模型的自动分析和验证的工具，实现由 l 作流模型到s p i n p r o m e l a 模型的自动转化。 通过本课题研究，欲得出使用u m l 活动图对工作流模型进行建模，并使用 模型检测工具s p i n 对模型结构、语义进行验证的方法，为把模型检测这种形式 化验证技术应用于工作流设计提供一种方法。 1 3 论文结构 本论文分为七章。第1 章绪论，介绍了本课题的研究背景、论文的主要内容 和要实现的目标。第2 章介绍工作流技术相关概念及其发展现状。第3 章介绍了 模型检测的相关理论和应用，对模型检测工具s p i n 的工作原理、p r o m e l a 语言及 工具中l t l 公式的表示方法做了较详细的阐述。第4 章对统一建模语言u m l 及 元数据交换标准x m i 作简单的介绍，提出基于u m l 的适用于模型检测的工作 流模型建模方法，定义模型的形式化描述。第5 章对工作流模型进行，提出了使 用模型检测技术对工作流模型正确性进行分析验证的方法，并将该方法应用与两 个工作流实例模型的验证。第6 章给出了自动分析工具体系结构和实现方案。第 7 章对本论文工作进行总结，指出下一步研究的方向。 第7 页 镍一章t - 作流概述 第二章工作流概述 工作流技术早在上个世纪9 0 年代成为计算机应用领域的一个研究热点。工 作流技术的历史可以追溯到2 0 世纪7 0 年代，它的概念起源于生产组织和办公自 动化领域，针对r 常工作中具有固定程序的活动而提出。其目的是通过将工作分 解成定义良好的任务、角色，按照一定的规则和过程来执行这些任务，并对它们 进行监控，以提高办事效率，降低生产成本，最终提高企业的竞争力。 2 1 工作流术语 一、工作流的定义 工作流( w o r k f l o w ) 的概念是在提高工作效率的研究中而产生的，目前仍没有 统一的定义。以下足它的部分描述【”。 ( 】) 工作流是指整个或部分在计算机支持下的全自动或半自动化的经营过 程。根据系列过程规则，文档、信息或任务能够在不同的执行者之问进行传递 与执行。这是工作流管理联盟( w o r k n o wm a n a g e m e n tc o a l i t i o n ) 给工作流下的定 义。 ( 2 ) 工作流是经营过程中可运转的部分，包括任务的顺序以及出谁来执行、 支持任务的信息流、评价、与控制任务的跟踪、报告机制。 ( 3 ) 工作流是涉及到多任务协调执行的活动，这些任务分别由不同的处理 实体来完成。一项任务可通过各种形式来定义需要做的某些工作。用来执行任务 的处理实体可以是人，也可以是计算机系统。 ( 4 ) 工作流是一系列工作的偏序集。工作的序列可以有多种方式，比如工 作x 与y 满足x s t a t e = s t a t e + 1 ) 3 p r o c t y p eb ( ) ( s t a t e = = 1 ) 一 s t a t e = s t a t e l 4 i n i t r u n a ( ) ；r u n b ( ) 图3 - 2 一个简单的p r o m e l a 程序 第一行定义了一个b y t e 类型的全局变量，初始化为1 ；第二行、第三行分别 定义了名为a 、b 的进程，这两个进程当s t a t e = l 时，分别对s t a t e 做加1 和减1 第1 5 页 第三章模型检测 的操作；第四行为一个相当于c 语言程序中m a i n ( ) 的进程i n i t ，它的任务是 启动进程a 和进程b 。 本节的剩余部分将对p r o m e l a 的主要内容做介绍。 1 、数据类型 p r o m e l a 中的数据类型包括：i n t 、b o o l 、b y t e 、s h o r t 和i n t ，它们对应的取值 范围如图3 3 所示。 b i t1 u n s i g n e d 01 b o o t1 u n s i g n e d 01 b y t e 8 u n s i g n e d 02 5 5 s h o r t16 s i c l n e d一2 6 1 5 2 “1 5 - 1 ” i n t3 2 s i一2 “3 1 “ 一1 c l n e d 23 1 幽3 - 3p r o m e l a 基本数据类型 2 、数组变量 p r o m e l a 中变量可被声明为数组。比如： b y t es t a t e n 】 声明了一个有n 个b y t e 类型的变量的数组，数组的第n 个元素可以s t a t e n 的形 式访问，其中n 的取值范围为0 ，1 ，n l 。 3 、进程 为了执行一个进程，用户必须能够命名它、定义它的类型并且将它实例化。 可以实例化的所有类型的进程都是在p r o c t y p e 声明中定义的，p r o c t y p e 定义只是 声明进程行为，而不执行该进程。 p r o m e l a 程序最初只有一个类型为i n i t 的进程执行，i n i t 进程必须显式声明， 它的作用相当子标准c 程序的m a i n ( ) 函数。通过元操作符r u n 来实例化一个给 定进程类型的副本。如图3 2 所示。 一个进程主要通过两种方式来与其它进程进行交互，一种方式是通过访问和 操作共享全局变量的来进行交互，另一种方式是通过消息通道来与其它进程进行 交互。 4 、消息通道 消息通道用于建模从一个进程到另一个进程的数据传输，通过使用关键字 c h a n 定义。消息通道可以被局部声明或全局声明。例如 第1 6 页 一 望三至竖型堡型 c h a na ，b ： c h a nc 3 】； 第一条语句声明了a 、b 两个通道，第二条语句声明了一个明为c 的通道数组。 通道传递的消息可以有多个域，如 c h a nq n a m e = 1 6 o f b y t e ，i n t ，c h a n ，b y t e ) 这条语句定义了一个可以存储1 6 条消息的通道，每条消息由四个域组成，这四 个域的数据类型分别为b y t e 、i n t 、c h a n 和b y t e 。 5 、发送与接受消息 p r o m e l a 语言分别定义了发送消息和接受消息的语句。语句 c h a nc h a n n a m e = 1 0 lo f i n t ： 定义了一个可以存放1 0 条消息类型为i n t 类型数据的通道。语句 c h a n n a m e ! a 表示把一个消息a 放入消息通道c h a n n a m e 的消息序列的末端，即发送消息。语 句 c h a n n a m e ? b 表示从消息通道的前端取出一条消息，并把它存入变量b 中。发送操作只有在通 道未满的情况下才是可执行的；接收操作只有在通道非空的情况下才是可执行 的。 使用容量为o 的通道可以定义同步通讯，比如语句 c h a np o r t = l o 】o f b y t e ) 语句定义的通道只能传递而不能存储单字节的消息。程序中语句 p o n1 1 2 3 可执行当且仅当程序中存在一个形如 p o n ? a 的语句与之对应。 4 、控制流程 p r o m e l a 的流程控制语句主要有选择结构语句、循环结构语句和跳转语句。 ( 】) 选择结构语句 p r o m e l a 语言通过i f f i 语句来表示选择，比如 j f 第1 7 酉 第= 章模型检测 ：( a = = b ) 一 o p t i o n l ：( a ! = | b ) 一 o p t i o n 2 i f 以上语句包含两个执行序列，每个序列以双冒号开头。只有当某个序列的第 一条语句可执行时候，该序列才会被选择执行。如果有超过一个执行序列的第一 条语句可执行，程序将不确定的选择一个序列执行。如果所有序列第一条语句都 不可执行，j f 语句将被阻塞，直至至少有一+ 个序列可以执行为止。 ( 2 ) 循环结构语句 p r o m e l a 语言通过d o o d 语句来表示循环，比如 d o ：c o u n t = c o u n t + l ：c o u n t = c o u n t 一1 ： ：f c o u n t = = o ) - b r e a k o d 此循环结构中的c o u n t 变量将不确定的做加l 或减l 的操作，直到当c o u n t - - o ， 才可能执行第三个语句序列，当执行到b r e a k 语句，才跳出该循环。循坏语句除 了执行次数与选择语句不同之外，其执行方式与选择语句相同。 ( 3 ) 跳转语句 p r o m e l a 语言保留了改变程序语句执行顺序的跳转语句g o t o 。g o t o 是除b r e a k 语句外跳出循环的另一个语句。 5 、p r o m e l a 语句的可执行性 在p r o m l a 语言中，条件与语句没有区别，单独的布尔条件也可以作为一条 语句。语句的执行取决于它的可执行性。可执行性是p r o m e l a 程序基本的同步机 制。p r o m e l a 程序中，语句或者是可执行的，或者是阻塞的。如果一条语句被阻 塞，它将被挂起直到它变为可执行为止。对以下的一个循环 w h i l e ( ai _ b ) s k i p 产等待a - - b8 ， 用p r o m e l a 语句可直接表示为 ( a b ) 第1 8 页 第三章模型检测 一个条件是可以执行( 或通过) 的当且仪当它是成立的，如果不成立，则被 阻塞直到它变为成立为止。 赋值( a s s i g h t m e n t ) 、声明( d e c l a r a t i o n ) 、断言( a s s e r t ) 、以及跳过( s k i p ) ，跳 转( g o t o ) 和断开( b r e a k ) 语句总是可执行的。 语句的可执行性在接收消息中有重要的应用。在消息接收语句中，一些参数 可以是常数，如 c h a n n a m e ? c o n s1 ，v a r 2 ，c o n s 2 在这种情况下，当且仅当接收语句的消息常数域与接收到的消息的对应域数据相 匹配时，语句才可被执行。否则，语句将被阻塞，试图执行此语句的进程将停止 运行直到该语句可执行或另一条可代替的语句可执行为止。 6 、标签 在验证模型的性质时，e n d 标签、p r o g r e s s 标签有着重要的应用。 ( 1 ) e n d 标签 在p r o m e l a 程序中，正常的结束状态应该是所有的进程到达了程序体的结尾， 并且所有的消息通道都是空的。但是不是所有的p r o m e l a 进程都会到达进程体的 结尾。一种可能就是进程处于一个循环状态，当有新的输入到达时执行相应的活 动。为了使模型检测的验证器知道，当程序结束时某个进程处于这种状态也是合 法的，这时就可在相应的某个语句前使用e n d 标签。 ( 2 ) p r o g r e s s 标签 p r o g r e s s 标签用于标识在程序推进的过程中必须经过的一条语句。程序中任 何不包含有此类标签的语句的无限循环，都被认为可能产生饥饿循环。 7 、断言( a s s e r t i o n s ) 断言用于描述当程序运行到当前语句是必须满足的性质，这些性质通常是一 些布尔公式，如 a s s e r t ( a = = 0 ) 如果句尔公式成立，则该语句对结论不产生任何影响；若不成立，s p i n 将在验证 后报告一个错误。 三、s p i n p r o m e l a 中的u l 公式 设p 是个原子命题，s p i n p r o m e l a 中的u 1 公式f 表示如下： f ：= p i t r u e i f a l s e i ( f ) l f b i n o p f i u n o p f 第1 9 页 第三章模型检测 其中： u n o p ：= 【1 ( a l w a y s ，对应线性时态逻辑中的g ) l ( e v e n t u a l l y ，对应线性时态逻辑中的f ) l ! ( 逻辑否定) b i n o p ：= u ( s t r o n gu n t i l ，对应线性时态逻辑中的u ) i ( 逻辑与) ( 逻辑或) i _ ( 蕴涵) i ( 等价) s p i n 允许用户在命令行中或在x s p i n 窗口中以设置验证参数的形式输入u 1 公式。如 s p i n f 【1p 对公式中出现的命题，可通过如下方式定义： # d e f i n e p ( a b ) # d e f i n ep ( 1 e n ( q ) 5 ) # d e f i n ep ( r o o t l a b e l ) 其中a 、b 为变量名，q 为一通道名，r o o t 为一进程名，它们都必须被全局的声明。 l a b e l 为r o o t 进程中某条语句的标签。 四、s p i n 可验证的性质 s p i n 可对系统是否具有以下性质进行验证。 ( 1 ) 死锁( d e a d l o c k ) 死锁是分布式系统中必须考虑的一个问题，通常是指 多个进程因竞争有限资源而形成的一种僵局。s p i n 能检测出系统中在任何情况下 的可能存在的死锁。 ( 2 ) 断言违反( a s s e r t i o nv i o l a t i o n ) 当程序执行到某个a s s e r t 语句，若断言中 的布尔公式不成立，s p i n 将报告一个错误。 ( 3 ) 死代码( d e a dc o d e ) 对任何情况下都不会执行的代码报告错误。 ( 4 ) 安全性质( s a f e t yp r o p e r t y ) 安全性对许多系统至关重要。用户可以定义 某些被认为是不安全的状态，使用s p i n 检测系统是否永远都不会进入这些状态。 ( 5 ) 活性( 1 i v e n e s sp r o p e r t y ) 用户可定义一个所谓“好”的状态，检测系统 第2 0 页 第三章摸型榆涮 是否最终会到达此状态。 对以上的验证性质，s p i n 提供了不同的验证参数供用户选择使用，部分验证 性质需要使用l t l 公式描述。s p i n 将对检测出的错误保存反例路径，供用户分 析使用。 箱2 i 页 第p v 章丁作流模型的u m l 建模 第四章工作流模型的u m l 建模 工作流模型是对工作流的抽象表示，也就是对经营过程的抽象表示。工作流 模型应该完整地提出支持工作流定义的概念，为建模用户提供工作流定义所需要 的组件或元素。u m l 是一种面向对象的、可视化统一建模语言，u m l 活动图为 描述工作流提供了很好的机制。 本章在对u m l 的语义、表示方法极其扩展机制做简单介绍的基础上，参照 工作流管理联盟提出的一个过程元模型，提出了以模型检测为目的的使用u m l 活动图的工作流建模方法，并介绍了u m l 活动图的基于x m i ( x m l m e t a d a t a i n t e r c h a n g e ，x m l 元数据交换) 标准的x m l 文档，定义了工作流u m l 模型的 形式化描述，为引入模型检测技术验证工作流做铺挚。 4 1u m l 简介 统一建模语言( u n i f i e dm o d e l l i n gl a n g u a g e ，u m l ) 硼是一种面向对象的、 可视化建模语言，其目的是建立统一的面向对象丌发方法，具有易于使用、表达 能力强，进行可视化建模，具备扩展和专用化机制，对特殊领域系统建模时不需 要对核心概念进行修改等优点。 4 1 1u m l 的主要内容 作为一种建模语言，u m l 的定义主要包括u m l 语义和u m l 表示法两个部 分。 ( 1 ) u m l 语义描述基于u m l 的精确元模型定义。元模型为u m l 的所有 元素在语法和语义上提供了简单、一致、通用的定义性说明，使开发者能在语义 上取得一致，消除了因人而异的最佳表达方法所造成的影响。此外u m l 还支持 对元模型的扩展定义。 ( 2 ) u m l 表示法定义u m l 符号的表示法，为开发者或开发工具使用这些 图形符号和文本语法为系统建模提供了标准。这些图形符号和文字所表达的是应 用级的模型，在语义上它是u m l 元模型的实例。 标准建模语言u m l 定义了下列五类图。 第2 2 页 第叫章丁作i ；l 模型的u m l 建模 ( 1 ) 用例图( u s ec a s ed i a g r a m ) 从用户角度描述系统功能，并指出各功能 的操作者。用例图只考虑系统应提供什么样的功能，对功能内部具体实现不作考 虑。 ( 2 ) 静态图( s t a t i cd i a g r a m ) 包括类图、对象图和包图。其中类图描述系统 中类的静态结构。对象图是类图的实例。包用于描述系统的分层结构。 ( 3 ) 行为图( b e h a v i o rd i a g r a m )包括状态图和活动图，专注于描述系统的 动态模型和组成对象问的交互关系。状态图描述类的对象所有可能的状态以及事 件发生时状态的转移条件。而活动图描述满足用例要求所要进行的活动以及活动 间的约束关系。本文使用活动图描述工作流模型。 ( 4 ) 交互图( i n t e r a c t i v ed i a g r a m ) 交互图描述对象间的动态交互关系，包括 顺序图和协作图。 ( 5 ) 实现图( i m p l e m e n t a t i o nd i a g r a m ) 包括构件图和实旌图，分别描述了 一组构件之间的组织和依赖关系和定义系统中软硬件的物理体系结构。 4 1 2u m l 的扩展机制 u m l 的扩展机制允许用户以受控的方式对语言进行扩展，这些机制包括构 造型、标记值和约束。 ( 1 ) 构造型( s t e r e o t y p e ) 是对u m l 词汇的扩展，允许创建与已有的构造 块而针对特定问题的新种类的构造块。在图形上，把构造型表示成用书名号扩起 来的名称，并把它放在其他的元素名之上。 ( 2 ) 标记值( t a g g e dv a l u e ) 是对u m l 元素特性的扩展，允许在元素的规 格说明中创建新的信息。 ( 3 ) 约束( c o n s t r a i n t ) 是u m l 中限制一种或多个元素语义的规则。约束 可以附加在类或对象上，并且经常附加在关系上，约束参与关系的类或对象。 4 2 工作流过程元模型 工作流模型是对经营过程的抽象表示，由于工作流需要在计算机环境下运 行，因此建立相应的工作流模型就是必不可少的。理想的工作流模型能够清楚地 定义任意情况下的工作流，能够适应用户在建模过程中所提出的各种要求。 第2 3 页 第四章t 作流模型的u m l 建模 工作流管理联盟提出了一个工作流的过程元模型( m e t a _ m o d e l ) ，其结构如图 4 一l 所示。 图4 - 1w f m c 的过程元模型 模型定义了如下基本实体： ( 1 ) 工作流定义( w o r k f l o wd e f i n i t i o n ) 也称过程模型，由过程分析、建模 和定义工具生成，并由工作流引擎解释执行。 ( 2 ) 活动( a c l i v i t y ) 活动是组成工作流的基本元素，对应于企业经营活动 中的任务，反映完成企业经营过程需要执行哪些操作。一个工作流也可看成由若 干活动按特定顺序执行的过程。其属性包括活动名称、类型( 子流程、原子级活 动等) 、活动执行的前后条件等。 ( 3 ) 转换条件( t r a n s i t i o nc o n d i c t i o n ) 包含过程执行的前、后条件，活动的 执行条件等。 ( 4 ) 工作流相关数据( w o r k f l o wr e l a t i v ed a t a ) 工作流管理系统根据工作流 相关数据确定过程实例状态转换的条件，进行过程的推进。工作流相关数据可被 外部应用访问并修改，其属性包括数据名称、类型、值等。 ( 5 ) 角色( r o l e ) 角色主要根据企业组织模型，描述企业经营过程中参与操 作的人员和组织单位。其属性包括角色名称、组织实体。 ( 6 ) 被激活的应用( i n v o k e da p p l i c a t i o n ) 在过程描述中，一个活动可能对 应一个或多个应用，这些应用在过程执行过程中被工作流执行服务( 工作流引擎) 所调用。 第2 4 页 第四章1 ：作流模型的u m l 建模 4 3 工作流模型的u m l 描述 u m l 活动图为描述工作流提供了很好的机制，本节参照工作流管理联盟定 义的过程元模型，使用u m l 活动图建模工作流，并给出了一个实例。模型检测 工具将以此模型为输入对工作流进行分析检测。 4 3 1 使用u m l 活动图描述工作流 一般情况下，u m l 活动图用来描述用例、对象和对象方法中所包含的动态 行为。它根据状态的变化来捕获要执行的动作或活动以及它们的执行结果，显示 从活动到活动的流。u m l 活动图也为描述工作流提供了很好的机制，本节将用 活动图来描述工作流模型中基本实体。 ( 1 ) 活动节点 对应工作流模型中的活动。u m l 使用一个圆角矩形表示活动，每个活动有 一个名字作为活动标识。有两个特殊的活动节点，分别表示工作流开始和结束。 ( 2 ) 分支节点 描述了工作流基于某个布尔表达式的可选择路径。u m l 用一个钻石形束表 刁i ( 3 ) 同步棒节点 对工作流的并发流进行描述。u m l 中使用同步棒一条粗的水平线表示。 有分叉和汇合两种情形。分又有一个进入转移和多个离去转移，表示多个控制流 并发执行；汇合有多个进入转移和一个离去转移，表示控制流的同步，直到所有 的流到达汇合处，方可转移到下一活动。 ( 1 3 活i 栉点 同步捧节点 分支节点 图4 2 活动图中的节点 ( 4 ) 转移 当一个活动结束时，控制流会马上传递给下一个活动。转移用来说明这样流， 显示从一个活动到下一个活动的路径。它的图标是一条实箭线。 第2 5 页 第四章工作流模型的u m l 建模 一个转移可以用促使转移发生的条件和事件等描述，表示只有当该事件发 生，且满足转移条件时，控制流方可从当前活动转向下一活动。转移条件用稚尔 公式描述，在这里我们约定布尔公式中变量初值为0 。一个事件可以是某业务组 织完成某个活动后向另一个业务组织发出的消息，意在请求其开始相应的某个活 动，使用一个有意义的字符串表示。 ( 5 ) 泳道 对活动图的活动状态进行分组，每组有共同的执行活动的业务组织，每个组 称为一个泳道，对应过程元模型的角色。泳道用纵向矩形来表示。属于一个泳道 的所有活动均放在其矩形符号内。泳道的名字即一组活动的执行组织的名字放在 其矩形符号的顶部。 ( 6 ) 构造型 u m l 扩展机制的一种，允许用户在模型中使用u m l 元模型不支持的词汇 描述系统。最简单的构造型就是用一个由书名号括起来的名称表示，把它置于被 说明的元素名上方。为更好的描述工作流性质，本文定义了三种类型的构造型， 以方便检测工具对模型性质的捕捉和检验： 布尔表达式类型的构造型：表明工作流中某个活动必须满足的性质，如 c h e c k p a s s = = o ) ) ，c h e c k p a s s 为用户定义的工作流变量，约定所有变量 初值为0 ； e n d 和p r o g r e s s 构造型：e n d 构造型表示当控制流到达包含此构造型的状 态可认为所属泳道的活动正常结束，活动中包含p r o g r e s s 构造型表示包 含此活动的循环控制流是合法的； l a b e l 构造型：用于标记此活动可能会在描述模型性质的l t l 公式中涉 及到。 当一个活动需要标记多个构造型时，用“”把它们隔开，如( ( p r o g r e s s l a b e l ) ) 。 4 3 2 工作流u m l 描述的优点 使用u m l 描述的工作流模型有如下好处： ( 1 ) u m l 活动图提供了标准的图形元素，具有较强的直观性，而且它是基 于事件的，与传统的流程比较相似，更接近人们对工作流程的直观理解： 第2 6 贞 第四章r t 作流模型的u m l 建模 ( 2 ) u m l 活动图能够把工作流过程涉及到的业务组织表示出来，人们可以 非常直观地从中了解到过程语境及交互的参与者，从而对工作流过程有更深刻的 了解； ( 3 ) 表达能力强，u m l 活动图能非常直接简单地描述六种工作流原语，并 能够描述一些比较复杂的逻辑结构，其扩展机制能够满足用户特殊的需要。 4 3 3 一个工作流模型的u m l 描述 如图4 3 所示，足一个使用r a t i o n a lr o s e l 2 6 1 建模工具描述的处理客户退款 要求的工作流。它有三条泳道，表示此工作流活动由三方业务组织完成。首先由 客户( c l i e n t ) 提出退款要求启动工作流，客户服务代表( c l i e n t _ s e r v i c e _ d e l e g a t e ) 接收客户请求，并对请求进行审核，若审核结果为不符合退款要求，则四复客户 表示拒绝退款：若审核结果为满足退款要求，则由客户服务代表为退款请求存档， 并要求财务工作者( f i n a n c e w o r k e r ) 开退款支票，最后通知客户请求被处理并 向其发送退款支票。最后客户接收到客户服务代表的回复，工作流结束。 s t a r l 1 a 磊函：f 一、 r e q u e s t r e f u n d 竺坐每7t、 r e f u n d m e n t c h e c “季。， c = ! 竺r e f ! u 竺n d m e 夕 一11 r e l u s e d 【c h e c 矗a s s 利一占 r e c or d 弋俪l t 零c c k | | 。曲。it p 一 | rec”譬x,m。dify-refundm i _ c r e a t e d | | fcaas=lhts e n d _ c h e c k 曲斟”) 脚而 7 u n 。d m e n lc h e c k 7 早( h a n d l e d”6 图禾3 处理客户退款请求工作流模型 第2 7 页 第旧章t 作流模型的u m l 建模 整个工作流模型使用了一个分支节点和两个同步节点。引入一个变量 c h e c k p a s s ，其初始值为0 ，可取值0 、1 和1 ，分别表示表示未进行审核、审核 末通过、审核通过三种情况。为了方便模型的验证，对请求退款 ( r e q u e s t r e f u n d m e n t ) 、更新退款记录( m o d i f y _ r e f u n d m e n t _ r e c o r d ) 以及发送退 款支票( s e n d _ c h e c k ) 活动使用了( 1 a b e l ) ) 构造型，另外发送退款支票活动还使 用了构造型( ( c h e c