一種基于產生式的流程模型分析方法

摘要：在深入分析業務流程模型和合理的抽象業務活動基礎上，提出了一種基于產生式的流程模型形式化分析方法，并提供了一種從一般流程描述到該模型的轉換方法；在此基礎上，推導了一系列行之有效的流程屬性驗證規則，并通過應用實際例子證明了所提出方法的有效性。

關鍵詞：業務流程模型； 分析和驗證

中圖分類號：TP3021文獻標志碼：A

文章編號：10013695(2007)04003705

業務過程的建模、分析和優化是支持企業業務過程重組的重要基礎。行之有效的模型分析方法是成功進行模型分析的關鍵技術問題。

業務流程重組的實質是企業根據市場需要以企業經營過程為核心重構企業的關鍵業務流程，并建立與其匹配的運行機制和組織結構，實現對經營過程的有效管理和控制。它一般分為五個階段，即項目規劃、企業經營過程建模、模型分析與優化、基于模型的業務經營過程重組實施和項目評價與監控。在這個過程中模型分析與優化是企業實施業務流程重組中非常重要的一個環節，對業務流程重組成功與否起著至關重要的作用。近幾年來，作為支持業務流程重組的重要技術的工作流技術得到了廣泛重視。但是由于工作流技術產生于實際應用，缺乏良好的理論基礎，應用工作流方法建立的企業經營過程模型缺乏必要且行之有效的模型驗證和模型分析方法。研究如何從理論上驗證所建立的過程模型結構的合理性，研究如何評價所建立的模型的性能和優化模型的方法就顯得尤為重要。

OncePI是中國科學院軟件所軟件工程中心自主研發的集工作流開發、監控和管理于一身的業務流程管理系統。該系統為企業應用提供了一個構建靈活、高效、自適應流程的平臺。OncePI引入面向服務的核心理念，通過將業務流程邏輯與實現各業務的應用相分離、管理流程參與者的相互關系、集成內部和外部資源以及監控和分析流程性能，實現了對業務流程整個生存周期的控制。這樣，管理者可以將精力集中于業務自身的優化、組合，從而適應不斷變化的商業環境。然而，如果一個業務流程管理系統沒有提供一套強有力的流程模型分析工具，流程模型的正確性、有效性和高效性就不能得到有效保證，為系統在現實的企業業務流程運行環境中的應用留下了障礙，特別是對于具有大規模業務流程的企業應用環境中，依靠人工對業務流程模型的維護，難以保證企業業務流程的正確性以及有效、高效的運行。

本文通過分析現有業務流程驗證概念和方法，結合OncePI系統在實際應用中面臨的流程分析和驗證需求，提出了一種基于產生式的流程分析模型以及相應的模型生成方法和驗證規則。在此基礎上，將這套方法應用于OncePI的流程模型分析和驗證之中，開發了一套有力的流程模型分析工具，為OncePI的集成流程設計和開發提供了可靠的保證。

1業務流程驗證概念和方法

工作流技術已經被越來越多的業界采用為商業應用和開發的關鍵技術。其主要特征是自動執行包括人員和自動型應用在內的業務流程。工作流模型是對工作流的抽象表示，也就是對經營過程的抽象表示。由于工作流需要在計算機環境下運行，建立相應的工作流模型是必不可少的。工作流模型應該完整地提出支持工作流定義的概念，為建模用戶提供工作流定義所需要的組件或元素。理想的工作流模型能夠清楚地定義任意情況下的工作流，能夠適應用戶在建模過程中所提出的各種要求。

定義和描述工作流模型的方法多種多樣，有業務流程語言如XPDL、BPML、BPEL等，還有形式化模型如EPCM模型、Petri網和工作流網等。概括起來可以分為語言描述方法、基于圖結構的方法、基于邏輯的方法、代數方法和ECA規則方法幾類^[1]。由于工作流模型的復雜性，目前還沒有有效的算法可以對工作流模型的正確性進行分析。目前已有的大部分工作流產品提供了流程模型的仿真和測試工具，也有一些研究者為流程模型的分析和驗證提出了各不相同的概念和方法。

現有的流程模型分析和驗證方法大概可以分為三類：

（1）基于圖形化簡的流程驗證方法

一般而言，基于圖形化簡的驗證方法適用于基于圖結構的流程模型描述方法^[2，3]，通過定義圖形結構的化簡規則，能夠在一定程度上驗證流程模型。在文獻[4]中，Sadiq W等人對有向無環圖(Directed Acyclic Graph，DAG)表示的業務流程證明其結構的正確性。在證明工作圖結構正確性的同時使用了如下五種歸約規則：終結符規約、順序規約、鄰接規約、閉合歸約和重疊歸約。如果一個工作流圖是正確的，則反復使用這些歸約規則可以將工作流圖歸約為空。但是由于圖形結構表達方式的局限性，這種流程模型驗證方法只能對部分流程結構中存在的問題進行分析和驗證，不能廣泛應用在一般的流程模型驗證問題中。文獻[5]中列舉了一個反例——交叉全連接的工作流圖，證明了雖然此工作流圖是正確的。但是使用重疊歸約規則不能消去圖中的交叉全連接結構，此流圖也無法規約為空。

（2）基于模型的流程分析驗證方法

文獻[6]中提出了用Petri網進行工作流建模的工作流網，將工作流模型的正確性歸納為工作流網的完整性，并在文獻[5]中提出了一種基于Petri網的圖形化簡方法輔助模型驗證。但是其提出的化簡步驟由于不具備完備性而不能完全驗證工作流模型的正確性。文獻[1]提到的基于模型檢查的流程分析方法具有很好的理論基礎。這種方法分為兩個階段：首先通過模型映射，將定義的流程模型映射到一種易于分析和驗證的有限狀態機模型上；在這個模型上使用相應的模型檢查器，探索整個狀態空間，檢查是否每一個系統狀態都滿足指定的流程屬性。由于這種方法只能應用在有限狀態機模型上，在流程模型的驗證中同樣只能部分地驗證流程屬性。

（3）基于仿真的流程分析方法

文獻[7]中提出了一種基于仿真的模型驗證方法，但它缺乏理論上的嚴格證明，而且當發現系統中確實存在沖突或死鎖時，并不能給出錯誤發生的確切位置（只是給出了一些輔助的檢測數據）。基于仿真的流程驗證方法，能夠結合具體工作流系統，仿真流程模型的執行過程，因而具有很好的實用性。但是其本身沒有嚴格的理論依據，并且依賴于具體的工作流系統，不具有普遍性。

OncePI的業務流程分析和驗證采用了一種類似于文獻[1]中提到的流程驗證框架，即將業務流程的驗證劃分為兩個階段：首先通過模型映射，將定義的流程模型映射到一種基于產生式的流程分析模型上；然后在這個模型上使用相應的模型化簡和變換規則，實現流程屬性的分析和驗證。這種基于產生式的模型以形式語言理論為基礎，能夠很好地表達業務流程并體現流程的過程特性。

2基于產生式的流程分析模型

一般而言，工作流是一類能夠完全或部分自動執行的業務過程。根據一系列過程規則，文檔、信息或任務能在不同的執行者之間傳遞、執行^[8]。而流程的業務過程模型通過流程模型中的各種實體及其約束關系(包括控制流和數據流)，將業務活動串聯起來，從而表達流程的業務過程。幾乎所有的流程模型都是基于活動（Activity）的，活動是具體執行業務任務的抽象。對于一個面向服務的業務流程管理系統而言，將活動的具體實現綁定到對某個服務的調用。這里的服務是一個抽象概念，可以是Web Service或者應用程序甚至是人工活動。這樣，可以把業務流程看做是服務的組合過程。下面本文使用“服務”這個概念指代流程模型中具體執行業務任務的實體。

2.1服務的抽象

如上文所述，在本文中服務指代流程模型中具體執行業務任務的實體。那么流程執行過程中，服務是如何完成業務任務的呢？粗略地說，服務請求方通過調用服務，與服務提供方之間發生交互，改變服務提供方和服務請求方的當前狀態，從而完成業務任務。因此，本文將服務定義為服務執行上下文狀態的一個映射?；谶@樣的理解，本文可以把服務形式化描述為

Service:(context，environment)->(context，environment)(1)

其中，Service是流程中的業務活動抽象，即服務；context是流程上下文的一個抽象，它代表服務調用方（流程實例）的上下文狀態；environment代表服務提供方（服務實現，如預定義的應用）執行服務的當前狀態。這樣，服務定義了執行過程中流程實例上下文狀態的躍遷及其對服務實現所處環境的作用。在以服務為著眼點時，可以合并服務提供方和調用方的狀態，通稱為服務執行的context；在以流程為著眼點時，可以忽略服務實現所處的環境狀態，而把context直接看做是流程本身的上下文狀態，這樣服務的形式化表述簡化為

Service: context->context(2)

從服務的角度重新考查流程的特征，可以定義服務的組合概念。本文把服務復合的邏輯稱為服務復合算子。

2.2服務算子及其性質

本文使用服務復合算子來描述流程中服務的復合邏輯。

什么是服務的組合呢？一種基本的認識是，多個服務的組合仍然可以被視為服務，即多個服務共同對服務運行環境的作用，可以等效地認為是一個新的服務對其的作用。這個新的服務即是組合的服務，服務組合的結果仍然是服務。

基于這樣一個認識，本文定義了服務算子來描述服務的組合。

定義1服務算子定義在服務域，并且其值域也是服務域，用來描述服務的組合

Operator: service*->service

其中*指定了算子的元數。

正如21節對流程中服務的組合過程所描述的那樣，分析了先前存在的大部分業務流程語言（XPDL、BPEL、BPML）和被研究的各種流程模式^[9～12]。順序組合和并發組合是兩種基本服務組合方式，其他的流程語言結構和流程模式都可以通過這兩種服務組合方式配合特定的路由邏輯復合而成。

（1）順序算子：它表達了服務的順序組合邏輯和流程中服務之間顯式的因果聯系。使用“#8226;”符號表示順序算子。服務的順序組合可以表示為

S=S1#8226;S2

這個表達式代表的語義是S(context)=S2(S1(context))，稱之為兩個服務的“積”。多個服務的順序組合使用類似的表達式S=S1#8226;S2#8226;S3。在不會引起誤會的場合也可以直接省略“#8226;”符號而直接將順序組合的服務并置在一起，如S=ab，S=abc。

（2）并發算子：它表達了服務的并發組合邏輯，在流程模型中被廣泛用來刻畫沒有因果聯系的活動的并發執行。服務的并發組合可以表示為

S=S1+S2

這個表達式代表的語義是S(context)=S2(context)+S1(context)，稱之為服務的“和”。如上文所述，context的合并時機和規則取決于流程引擎的具體實現。多個服務的并發組合使用類似的表達式S=S1+S2+S3。

（3）選擇算子：它用來表達流程中服務的路由選擇邏輯。許多類型的流程模型中存在這樣的路由邏輯；服務的選擇依賴于運行時具體的流程上下文內容。選擇算子被用來刻畫這種動態路由邏輯。首先，定義服務的動態選擇函數表示為

Eval: context->service

其中，context是流程中服務啟動時的上下文狀態；service是流程實例運行時選擇執行的服務分支；Eval函數定義了上下文狀態到服務分支的映射。在這個基礎上，服務選擇邏輯可表示為

S=Eval?S1|S2

這個表達式代表的語義是S(context)等于S1(context)還是S2(context)取決于Eval函數對context映射的結果。多個服務的選擇邏輯可以用類似的表達式表達S=Eval?S1|S2|S3。在靜態表達流程結構時，可以忽略選擇函數而把選擇表達式簡寫為

S=S1|S2|S3

從這個定義出發，可以得出選擇算子表達的是所謂的XOR選擇邏輯^[15]。從這個算子可以擴展出一些新的算子，用來表達很常見的一些流程模式，如While循環和DoWhile循環模式。本文使用閉包算子“S*”和正閉包算子“S+”來表達。

下面進一步分析這三種基本服務復合算子的性質?？紤]流程模型中服務的語義，結合上文中對順序、并發和選擇算子的詳細討論，針對算子的運算法則，有如下結論：

（1）順序算子不具備交換律，即一般情況下，S1#8226;S2≠S2#8226;S1；

（2）順序算子具有結合律，即(S1#8226;S2)#8226;S3=S1#8226;(S2#8226;S3)；

（3）并發算子具有交換律，即S1+S2=S2+S1；

（4）并發算子具有結合律，即(S1+S2)+S3=S1+(S2+S3)；

（5）選擇算子具有交換律，即S1|S2=S2|S1；

（6）選擇算子具有結合律，即(S1|S2)|S3=S1|(S2|S3)；

（7）順序算子與并發算子之間不存在分配律，即S1+S2#8226;S3≠S1#8226;S2+S1#8226;S3，S1#8226;(S2+S3)≠S1#8226;S2+S1#8226;S3；

（8）順序算子對選擇算子具有分配律，反之不具備，即S1#8226;(S2|S3)=S1#8226;S2|S1#8226;S3，S1|S2#8226;S3≠(S1|S2)#8226;(S1|S3)；

（9）并發算子對選擇算子具有分配律，反之不具備，即S1+(S2|S3)=S1|S2+S1|S3，S1|(S2+S3)≠(S1|S2)+(S1|S3)。

對于以上關于服務復合算子運算法則的結論，需要說明的是，設計到選擇算子的結論（5）、（6）、（8）、（9）中，如果將服務選擇函數納入考慮范圍之內，均必須重新定義新的選擇算子的選擇函數。這樣才能夠保證變換前后的等效性，但是這一要求并不影響流程過程的分析。因此，在使用這些算子作流程過程分析時，仍然可以使用以上的運算法則。

對比傳統業務流程模型可以看出，這里提到的服務算子實際上替代了所謂“啞元”這一概念。傳統的工作流模型把服務（活動）組合與具體的服務混為一體而不加區分，從模型本身就增加了流程分析的難度。本文使用服務復合的概念，可以建立較為清晰的服務復合流程模型。

2.3產生式模型

在服務和服務復合算子概念的基礎上，可以開始建立基于產生式的服務復合業務流程模型。

在流程的產生式模型中，終結符表示流程的原子服務，非終結符表示流程的復合服務；符號之間通過上文所述的三種基本算子連接構成表達式；非終結符結合對應的表達式構成產生式；一組完備的產生式構成了流程的過程模型。注意其中完備的含義是指產生式中涉及到的非終結符均有對應的表達式，即產生式集中的任何一個非終結符至少有一次出現在產生式的左部。流程的過程模型可以形式化地定義如下。

定義2流程的過程模型F是一個四元組：（A，C，P，S0）

其中，A是流程的原子服務集合，非空有窮集合，任何s∈A均是流程中的原子服務；C是流程的復合服務集合，非空有窮集合，任何S∈C都是流程中的復合服務；P是流程的產生式集合，非空有窮集合，P中的元素均具有S→α的形式，稱為產生式。S∈C，α為服務集合（A∪C）上的表達式。服務之間的運算符包括順序算子、并發算子和選擇算子，對于產生式集合P，不存在產生式S1→α，S2→β，使得S1=S2。S0是流程的開始符號，S0∈C。

在產生式模型中，把業務活動抽象為服務，用產生式來表達服務的復合，使用終結符表示原子服務；在流程模型中，它們沒有結構，不可細分，用小寫字母表達，如a、b、c等。本文使用非終結符表達復合服務；在流程模型中，它們是有結構的服務，可以使用產生式生成更細粒度的服務，用大寫字母表達，如A、B、P、Q等。

結合形式語言理論和上文給出的運算法則，可以對流程模型進行類似的歸約或稱之為派生，如V→aW，W→b|c=>V→a(b|c)→ab|ac。實際上，在原子服務集合和算子集合{#8226;，+}上定義了一個服務復合的形式語言，流程的產生式組模型就是這個語言的文法。

使用這種形式語言表示方法，不僅可以使用產生式文法來表達流程的靜態結構，而且可以通過產生式的派生，得到流程的派生樹，從而表達流程的運行時動態行為。比如，流程P的產生式集合是{P→A+B，A→a|b，B→c|d}，則流程的派生樹有四個：P=>a+c，P=>a+d，P=>b+c，P=>b+d。

下面給出一個流程實例來說明如何使用產生式模型表達流程。圖1中使用有向圖繪制的流程圖表達了一個常見的申請處理流程。首先一個申請在“編輯申請”活動中被編輯提交；然后申請被同時遞交給活動“預算審核”和“權限審核”，進行申請的預算審核和申請內容權限的校驗；審核結果將被校驗以確定申請是否通過審核；通過審核則進入“批復申請”活動完成申請的批復，否則申請將被退回申請者編輯修改申請。在這個流程中，使用前面所說的產生式模型，則流程表示如下：

列出組成流程的原子服務。其中a為“編輯申請”，b為“預算審核”，c為“權限審核”，d為“批復申請”。根據圖1中表達的流程過程邏輯，流程可以簡單地表示為

Process P：S→LdL→(T)+T→aFF→b+c（3）

對式（3）進行歸約，可以得到流程的形式語言表達式：

S→[a#8226;(b+c)]+#8226;d（4）

以產生式模型為基礎，可以在這個模型上研究流程過程模型的分析和驗證方法。下面討論如何從常見的流程表達形式自動化地轉換為基于產生式的形式模型，以及模型上的派生規則和流程屬性判定方法。

3模型的生成和驗證

使用基于形式化模型的業務流程分析驗證方法，首先需要從用戶定義的業務流程模型生成對應的流程形式化模型。業務流程的表達方式多種多樣，因此，需要為不同的流程表達方式制定不同的自動化翻譯規則。OncePI中使用一種基于XPDL10改進的并與其極其類似的語言來表達業務流程。本章以OncePI中的流程表達方式為例，制定了自動化翻譯規則，生成流程的形式化模型。

3.1產生式模型的生成

在表述一個流程時，一般直接使用一組產生式表示流程的過程邏輯。出現在產生式中的小寫字母是終結符，表示流程的原子服務；出現在產生式中的大寫字母是非終結符，表示流程的符合服務。為了表示的方便，可以把選擇算子的每一個分支使用一個產生式來表示，這樣產生式的右部中就可以只有兩種算子，即順序和并發。

使用產生式模型表達流程簡單靈活、易于構造。可以根據業務流程中活動的相互依賴關系直接建立流程對應的產生式組，也可以通過一定的規則轉換現有的表達方式而得到。針對OncePI Studio中基本的工作流模式，定義一組轉換規則，簡單描述如下：

規則1

（1）對流程中每一個應用型活動，賦予一個終結符。

（2）對流程模型中每一條躍遷，賦予一個非終結符。

（3）對規則（2）得到的每一個非終結符S，生成一個產生式S→α。表達式α生成方法如下：

①如果S對應的躍遷指向的是一個應用型活動s，則α=sT。其中T是從s出發的躍遷所對應的非終結符。

②如果S對應的躍遷指向的是一個流程結束活動，則α=E。其中E表示流程的終結。

③如果S對應的躍遷指向的是一個并發分支B，則α=B1+B2+…+Bn，即B的所有分支躍遷的和。

④如果S對應的躍遷指向的是一個排他分支X，則α=Eval?B1|B2|…|Bn。其中Eval是分支X的選擇函數。也可以把這個產生式拆分簡寫為多個產生式：S→B1，S→B2，…，S→Bn。

⑤如果S對應的躍遷指向的是一個排他合并U，則α=T。其中T是從U出發的躍遷。

（4）如果若干個躍遷指向的是同一個并發同步節點W，則生成一個表達式S1+S2+…+Sn→T。其中S1，S2，…，Sn是指向W的所有躍遷，T是從W出發的躍遷。

（5）將從流程的開始活動出發的躍遷對應的非終結符作為產生式組的開始符號。

需要額外說明的是，對于基于圖結構的流程表達方式，按照類似上述的規則（4），并發分支的同步合并節點會轉換成為S1+S2→T這種不能嚴格符合定義的產生式。在這里引入新的化簡規則（在3.2節的產生式歸約中將應用到這一規則）：

R1→α#8226;S1，R2→βS2，S1+S2→T＝>R1+R2→(α+β)T

從這個例子中可以看出，只需使用簡單的規則就可以實現產生式模型到其他流程表達模型的變換。在很多需要變換流程表達方式的場合，可以制定這種簡單的規則來實現。下文在作流程分析和驗證時，將會用到這種規則，將有向圖結構的易于設計者理解的流程模型轉換為便于流程分析驗證的形式化模型。

3.2產生式歸約規則

流程的動態分析通過產生式的派生和數據流依賴關系分析來獲得流程的控制流行為特征。

使用與規則1類似的規則，可以從傳統的圖結構流程模型自動化地轉換為形式化的產生式模型。下面討論如何使用產生式模型將一般的流程模型轉換為結構良好的流程，并且在這個過程中可以看到，流程的一些特性包括結構上的沖突等會在模型變換過程中被分析出來。

首先給出流程產生式模型歸約的規則：

規則2

（1）（合并）合并左部重復的產生式，使其符合產生式左部的唯一性。

（2）（可達符號集）可達符號集定義為：開始符號屬于可達符號集；出現在可達符號集中符號的產生式右部的非終結符屬于可達符號集。

（3）（連通流程）除非產生式組中所有的非終結符都屬于可達符號集；否則，本流程中存在不能被執行的部分，流程中各部分不連通。

（4）（終結消元）對任何產生式S→α，若S不是開始符號，且α中不包含非終結符，則將這個產生式代入其他任何右部包含該產生式左部非終結符的產生式中，消去此非終結符。重復執行此規則直到不存在這樣的產生式。將符號E看做終結符號。

（5）（選擇表達式）使用算子運算法則中的分配律化簡剩余產生式的右部為選擇表達式，即表達式中所有的選擇算子均在表達式樹的第一層，形如S→α|β|γ。

（6）（可終結符號集）若非終結符S的產生式右部的所有選擇分支中存在一個分支，其中只包含終結符和已經確定為可終結的符號，則S稱為可終結的符號。所有可終結的符號構成可終結符號集。

（7）（無限流程）若執行以上步驟后，產生式組中存在非終結符S，屬于可達符號集但不屬于可終結符號集，則本產生式表達的流程是一個潛在的不能在有限步歸約后結束的流程；否則，流程具有有界性。

（8）（簡單流程）整理終結消元的結果。如果剩余的非終結符僅有開始符號，則流程中不存在循環、遞歸等復雜流程結構，稱為簡單流程。

（9）（非終結消元）如果流程不是簡單流程，設剩余非終結符構成集合C，若存在非開始符號的非終結符S屬于C且S不出現在S的產生式的右部，將此產生式代入其他產生式中S出現的地方，消去非終結符S；重復執行此規則直到不存在這樣的S。

（10）（遞歸子集）不能被消元的終結符集合及其產生式構成了遞歸子集；更細致的分析可以定義最小遞歸子集及其階數、遞歸子集的劃分及其相互依賴關系。例如一階遞歸子集形如R→f(R)表達了一階遞歸結構，在首遞歸和尾遞歸的情況下可以退化為循環結構。

再看圖1中所示的流程。應用模型生成規則，產生對應的產生式組，然后使用上面的流程歸約規則，即得到了流程的最簡表達式（4），并且在規約過程中可以確定流程的有界性和結構特性。

下面使用上述規則來分析一個具有結構沖突的流程。圖2是使用OncePI Studio建立的一個新的申請審批流程。

該流程是一個典型的非結構化流程模型，它試圖通過將“格式化申請”的任務與“預算審核”的任務并發執行，從而提高流程的執行效率。然而，流程圖中“預算審核”活動可能否決申請要求，從而導致重新執行“編輯申請”活動。這樣，并發執行的多個“格式化申請”活動實例將使得并發同步活動m的同步語義模糊，出現結構沖突。下面展示如何使用流程的產生式派生規則分析流程結構沖突的過程。

首先，使用規則1生成流程模型對應的產生式組：

Process P：S→aRR→U1+U2U1→bW

U2→cXW→T|VV+X→Y（5）

Y→dZT→aRZ→E

然后使用算子運算法則按規則2對產生式組進行歸約。對流程式（5）使用以上規則，得到

S→aRR→baR+cX|(b+c)dE

在化簡過程執行到這一步時，從化簡結果可以看出，由于原流程設計上的缺陷，可能出現多個并發分支X的同步丟失。并發分支無法正確同步，流程存在結構上的沖突即同步丟失。

從上面給出的兩個實例可以看出，使用上述規則在對業務流程模型的生成和歸約過程中，已經能夠刻畫出流程模型的若干特性了，如有界性、結構沖突等。另外，通過歸約，還可以分析流程的循環、遞歸等結構，將一個基于圖結構定義的業務流程模型，轉換為另一個語義上等價的結構化流程模型來表示。

4結束語

業務流程模型的分析和驗證是工作流技術中重要的研究課題之一。本文在總結已有業務流程模型分析方法的基礎上，通過對業務活動的分析和抽象，提出了一種基于產生式的業務流程形式化分析模型，并且定義了流程化簡和流程屬性驗證規則，應用一些實例展示了這種流程分析模型在流程分析和驗證中的能力。要使用這種流程分析模型，首先可以根據工作流系統具體的流程定義，應用相應的轉換規則，自動化地得到流程的形式化分析模型；然后針對要驗證的業務流程屬性，選擇應用特定的流程屬性驗證規則來檢查模型的具體屬性，從而為業務流程的應用提供正確性、有效性的保證。

本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文。