（北京航空航天大學 計算機學院， 北京 100191）

摘 要：

提出一種可視化的約束規(guī)則建模語言(visual constraint modeling language， VCML)，采用XYZ/E語言作為邏輯框架，統(tǒng)一定義約束規(guī)則和業(yè)務過程兩種模型的形式化語義，為約束規(guī)則的自動驗證提供形式化基礎；然后基于模型檢驗(model checking)技術，簡要討論模型自動驗證的實現(xiàn)方法；最后通過一個應用實例說明業(yè)務過程約束的建模。

關鍵詞：業(yè)務約束;時序邏輯; 業(yè)務建模

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

文章編號：1001-3695(2009)04-1342-03

Verification ofbusiness process constraints based on temporal logic

GAO Jun-tao， ZHANG Li

（School of Computer Science Engineering， Beihang University， Beijing 100191， China）

Abstract:This paper proposed a kind of visual constraint modeling language for business processes， namely VCML and pro-ducted research on automatic verification technology. Used XYZ/E to formally define the VCML model and business process model. Described the business process in VPML(visual process modeling language)， then discussed to implement the method using model checking technology. At last， illustrated an example the modeling of business process constraint.

Key words：constraint rule;temporal logic;business modeling



為了適應外部環(huán)境的持續(xù)變化，企業(yè)必須不斷地改進業(yè)務過程，以保持核心競爭力[1]。然而企業(yè)在不斷調整自身業(yè)務過程的同時，其行為不可避免地受到諸多外界條件的影響和制約。這些外界條件可能來自于國家法律、法規(guī)、行業(yè)標準，以及風俗習慣，并不以企業(yè)的意志為轉移[2]。顯然，各種約束規(guī)則對業(yè)務過程的限制，對業(yè)務過程的設計和改進具有重要影響。特別是對于業(yè)務過程復雜、約束規(guī)則眾多的大型企業(yè)，在業(yè)務過程重組的過程中很難快速判斷業(yè)務過程是否符合所有約束規(guī)則，因此在不斷調整業(yè)務過程和約束規(guī)則的同時，快速準確地驗證業(yè)務過程是否符合約束規(guī)則，就成為企業(yè)成功實施業(yè)務過程改進或重組的必要條件。

約束規(guī)則的自動驗證要求業(yè)務過程和約束規(guī)則均采用形式化方法定義。然而目前描述約束規(guī)則的方法還比較隨意，通常采用自然語言說明，很難實現(xiàn)自動的約束驗證。因此有必要定義一種語義嚴格的建模語言，規(guī)范定義各種業(yè)務約束規(guī)則。而且約束規(guī)則的建模工作通常是由不熟悉IT技術的業(yè)務人員和領域專家完成的，因此該建模語言應該足夠簡單和直觀。企業(yè)外部環(huán)境會對業(yè)務過程產生多方面的影響，如業(yè)務過程結構、業(yè)務對象、資源配置等，而本文主要研究企業(yè)外部環(huán)境給業(yè)務過程的結構所造成的約束和限制。

本文提出一種可視化的約束規(guī)則定義語言VCML，結合可視化的業(yè)務過程建模語言(VPML)[3]討論業(yè)務過程約束的自動驗證方法。過程建模描述企業(yè)的具體運作方式，屬于敘述型(narrative)建模范式，通常采用Petri net或Pi演算作為其形式化基礎。約束規(guī)則是對企業(yè)行為性質和約束條件的定義，屬于聲明型建模范式，通常采用線性時序邏輯作為其形式化基礎[4， 5]。本文選用XYZ/E時序邏輯語言作為定義VPML和VCML語義的統(tǒng)一邏輯框架。XYZ/E是一種可執(zhí)行線性時序邏輯語言，既可表示系統(tǒng)的性質，又可表示系統(tǒng)的行為[6~8]。采用XYZ/E作為過程模型和約束規(guī)則模型的形式化語義基礎，可以在一個統(tǒng)一的邏輯框架下研究業(yè)務過程的約束規(guī)則，將過程模型是否滿足約束規(guī)則的問題轉變?yōu)榭疾爝壿嬏N涵表達式是否成立的問題。

1 XYZ/E語言

XYZ/E語言是線性時序邏輯語言的一種變型，是一種可執(zhí)行的時序邏輯語言，既可以表示系統(tǒng)的靜態(tài)語義，也可以表示系統(tǒng)的動態(tài)語義[6， 9]。XYZ/E在線性時序邏輯的基礎上，增加了一組時序操作算子，本文主要用到其中四個算子：下一時刻操作算子(next)“$O”、最終操作算子(eventually)“◇”、必然操作算子(always)“□”和直到操作算子(until)“$U”。

1.1 基本語言成分

XYZ/E的基本語言成分是條件元(conditional element)。每個條件元是一個時序邏輯式：

LB=y∧R@(Q∧LB=z)

（1）

其中：“ ”表示蘊涵；R和Q表示一階邏輯公式，分別稱為條件元的條件部分和動作部分；y和z分別表示條件元的定義標號和標號；符號“＠”為一個時序邏輯操作數，可以是下一時刻操作數“$O”，也可以是最終操作數“◇”。式（1）的直觀含義是：如果控制流LB走到標號y，并且用一階命題R為真，則下一時刻或最終命題Q為真，而且控制流LB轉到標號z。一個XYZ/E單元（unit）是由一組形式如式（1）的A1，…，AN，通過“;”連接而成：

□[A1，…，AN]where B（2）

其中：“;”表示邏輯合取“ ∧”；where部分的公式B是對整個單元的約束，where部分缺省時表示B＝$T（$T，$F分別表示布爾值真、假）；時序操作數“□”表示總是（always）。一個單元也是一個時序邏輯公式。

XYZ/E還可以表示一組進程P1，…， Pk并發(fā)執(zhí)行，其表達形式如式（3）。

LB=y∧R‖[P1，…，Pk](3)

控制流LB走到標號y處，如果前提條件R滿足，控制流分叉為并發(fā)的子控制流程LB1，…， LBk，對應于進程P1，…， Pk，該語句蘊涵如下假設：LB=y∧R◇(LB1=STOP1∧…∧LBk=STOPk∧LB=z)(LB1=STOP1∧…∧LBk=STOPk)∧LB=z$OLB=w。w是進程P1，…， Pk并發(fā)執(zhí)行結束后要轉入的標號。

1.2 通信命令

XYZ/E語言提供兩種通信命令：

輸入命令：LB=y∧RChNm?x∧$OLB=z

輸出命令：LB=y∧RChNm!e∧$OLB=z

其中：“ChNm”是信道名；x是變量；z是表達式?！癈hNm?x”表示由信道ChNm接收信息送入變量x中，數據與x的類型必須一致；“ChNm!e”表示由通道ChNm送出表達式e的值，數據與e的類型必須一致。

2 VCML語言

目前針對業(yè)務過程約束的研究還不多見，只有文獻[10]提出了兩種面向質量控制的過程約束方法。該方法通過擴展UML活動圖的基本圖元，提出一種約束規(guī)則與業(yè)務過程模型混合的模型圖。

企業(yè)的各種約束規(guī)則往往來源于政府法律、法規(guī)、環(huán)保條例、行業(yè)標準或現(xiàn)有技術條件等限制，在業(yè)務過程改進過程中，不受企業(yè)的意志支配。本文以航空制造業(yè)的成件入庫管理為例說明約束規(guī)則，由于航空制造業(yè)的產品價格昂貴和對高可靠性的要求，要求航空制造企業(yè)成件入庫時必須滿足如下條件:a)在入庫之前，必須經過驗收通道由收貨部人員負責驗收，并按進貨日期分類編號，按類別存檔備查；b)對庫存成品定期進行保質期和質量檢查，發(fā)現(xiàn)過期成品應及時處理。這些約束規(guī)則限制業(yè)務過程的范圍，但是并沒有直接指出應該采用哪種業(yè)務過程。以約束規(guī)則a)為例，雖然規(guī)則a)要求入庫活動之前，必須通過收貨部人員的驗收，但允許在驗收之后，先進行其他活動，然后再入庫。

因此，約束規(guī)則僅是外部環(huán)境對企業(yè)內部業(yè)務過程的一種限制，但不能根據約束規(guī)則直接推導出業(yè)務過程。企業(yè)在設計業(yè)務過程時，還要權衡很多其他因素，如生產周期、生產成本等。

經過對ISO9001標準[11]、航空制造業(yè)相關操作規(guī)范的調研，本文提出一種獨立的業(yè)務規(guī)則建模方法，支持企業(yè)五種常見約束規(guī)則，即存在規(guī)則、前驅規(guī)則、后繼規(guī)則、共存規(guī)則和互斥規(guī)則。由于采用約束規(guī)則與業(yè)務過程相分離的建模方式，模型更加簡潔直觀。

本章不僅給出VCML的可視化建模元素，并用XYZ/E定義其語義。為了方便業(yè)務規(guī)則模型語義的定義，首先給出一組公式。

occur>0(A) ：◇(LB＝A) （4）

occur>1(A) ：◇(LB＝A∧$O(occur>0(A)))（5）

occur>2(A) ：◇(LB＝A∧$O(occur>1(A)))（6）



occur>N(A) ：◇(LB＝A∧$O(occur>N-1(A)))（7）

式（4）定義活動A至少執(zhí)行一次，式（5）采用遞歸的方式定義活動A至少執(zhí)行兩次。依此類推，式（7）定義活動A至少執(zhí)行N次。

occurN-1(A)（8）

式（8）定義活動A的執(zhí)行次數最多不超過N-1次，但可以達到N-1次。

occurN(A) ：occur>N-1(A)∧occur

式（9）定義活動A的執(zhí)行次數正好為N次。

下面給出五種業(yè)務規(guī)則的語義定義：

a)存在規(guī)則是對業(yè)務過程中的業(yè)務活動執(zhí)行次數的約束，其語義可以定義為occur>0(A)。

b)前驅規(guī)則是指業(yè)務活動B執(zhí)行時，另一業(yè)務活動A必已執(zhí)行，否則活動B不能執(zhí)行。與過程模型中定義的活動依賴關系不同，前驅規(guī)則并不要求活動B的執(zhí)行緊跟活動A之后，它們之間可以有其他活動執(zhí)行。而且活動A執(zhí)行后，活動B可以不執(zhí)行。其語義可以定義為□(!（LB＝B）$U（LB＝A）)。

c)后繼規(guī)則是指業(yè)務活動A執(zhí)行后，另一業(yè)務活動B必將執(zhí)行，與前驅規(guī)則類似，后繼規(guī)則并不要求活動B的執(zhí)行緊跟活動A之后，它們之間可以有其他活動執(zhí)行。而且活動B可以在活動A未執(zhí)行的情況下單獨執(zhí)行。其語義可以定義為□(（LB＝A）→occur>0(B))。

d)共存規(guī)則是指如果業(yè)務活動A執(zhí)行過，則另一業(yè)務活動B必然已經或將要執(zhí)行。其語義可以定義為occur>0(A)occur>0(B)。

e)互斥規(guī)則是指如果業(yè)務活動A執(zhí)行，則另一業(yè)務活動B永不執(zhí)行;反之亦然。其語義可以定義為(occur>0(A)occur<1(B))∧(occur>0(B)occur<1(A))。

3 VPML語言

VPML是由北京航空航天大學計算機學院研發(fā)的一種可視化的業(yè)務過程建模語言。它不僅支持可視化的業(yè)務過程建模、靜態(tài)分析，還可以借助動態(tài)模擬技術，幫助企業(yè)用戶進行業(yè)務過程和資源配置的優(yōu)化。目前VPML已經在航空制造業(yè)得到了廣泛的應用[12， 13]。VPML詳細的語言規(guī)范參見文獻[3]。

3.1 VPML語法

由于篇幅所限，本文只討論與操作語義相關的VPML語法，而沒有考慮資源。任何包含組合活動的VPML模型，均可以等價地轉換為不帶組合活動的簡單VPML。

定義1 一個簡單VPML模型圖SP，是一個四元組(A， type， D，F(xiàn))。其中：

A是所有活動的集合。

type: A→{basic， andIn， andOut， orIn， orOut}是SP中活動的類型函數。

SP中所有狀態(tài)應該滿足類型約束:

stype≡def(a∈A#8226;type(a)=basic∨′type(a)=andIn∨

′type(a)=andOut∨′type(a)=orIn∨′type(a)=orOut)

其中V′表示不可兼析取連接詞。

D表示SP可以接收或生成的數據模式集合。

FA×D∪D×A表示數據流的集合。

SP中所有數據流應該滿足流約束:

sflow≡def(a∈A#8226;(type(a)=andIn∨′type(a)=orIn→|{a}×D∩F|≤1|)∧(type(a)=andout∨

′type(a)=orOut→|D×{a}∩F|≤1|))

一個合法的SP必須滿足語法約束：stype∧sflow。

3.2 VPML操作語義

在正式定義VPML語義之前，首先定義兩個函數。對于一個活動a∈A，它的輸入數據集合為inData(a)，它的輸出數據集合為outData(a)。其中:

inData(a)={d|(d，a)∈F};outData(a)={d|(a，b)∈F}。

定義2 semA(a)是用XYZ邏輯語言表示活動a的操作語義。

對于任一個活動a，定義輸入數據和輸出數據集合：inData(a)={din1，…，dinM}，outData(a)={dout1，…，doutN}。

如果type(a)=basic|andIn|andOut，則用XYZ表示，其操作語義為semA(a)：

din1#8226;count＞0∧…∧dinM#8226;count＞0

◇(a#8226;action∧LB=a∧dout1#8226;count=dout1#8226;count+

1∧…∧doutN#8226;count=doutN#8226;count+1∧din1#8226;count=

din1#8226;count-1∧…∧dinM#8226;count\\dinM#8226;count-1)

如果type(a)=orIn，則outData(a)={dout}，其操作語義為semA(a)：

din1#8226;count＞0◇(dout#8226;count=dount#8226;count+1∧din1#8226;count=din1#8226;count-1)



dinM#8226;count＞0◇(dout#8226;count=dout#8226;count+1∧

dinM#8226;count=dinM#8226;count-1)

對于任一個活動a∈A，如果type(a)=orOut，則inData(a)={din}，其操作語義為SemA(a)：

din#8226;count＞0∧(a，dout1)#8226;condition=$T

◇(dout1#8226;count=dout1count+1∧din#8226;count=din#8226;count-1)



din#8226;count＞0∧(a，dountN)#8226;condition=$T◇(doutN#8226;count=doutN.count+1∧din#8226;count=din#8226;count-1)

其中condition是orOut型活動輸出數據流上執(zhí)行條件。通常一個orOut型活動所有輸出數據流上條件是互斥的。

定義3 VPML過程模型圖SP到XYZ/E的語義轉換是一個映射semantics: SPs→XYZUNITs，SPs是基本VPML過程模型圖集，XYZUNITs是XYZ/E的單元集。若SP的活動集合為A={a1，…，aN}，則semantics(SP)=□[semA(a1)∧…∧semA(aN)]。

4 驗證方法

設φ是一個用表示約束規(guī)則的XYZ/E公式，M是用一個VPML過程模型。如果M滿足約束φ，則M｜→φ成立。筆者知道M｜→φ成立等價于公式M｜→φ是不可滿足的。所以要驗證過程模型M是否滿足約束φ，只需驗證公式M｜→φ是不可滿足的即可。

根據前兩章論述可知，M｜→φ是一個命題時序邏輯公式（PLTL公式），所以可以利用可滿足性判定工具STeP自動判定公式M｜→φ的可滿足性。

5 應用實例

本章利用一個例子說明業(yè)務過程約束建模方法。如圖2所示，針對某航空企業(yè)成件的入庫管理流程建立VPML過程模型M：inventory receipts management。接到到貨通知書后，首先由接收單位進行登記，形成一份器材入庫單；然后由檢驗員進行抽檢，如果產品合格則簽章、填寫入庫單、辦理交接簽收、入庫臺賬登記；否則出具意見、與開發(fā)商協(xié)調，根據協(xié)調結果決定退貨或再繼續(xù)入庫。

semA(A1)≡def(D1#8226;count＞0◇(LB=

A1∧(D2#8226;count=D2#8226;count+1)∧D1#8226;count=D1#8226;count-1))

由于篇幅所限，在此不給出每個活動的語義。最終，入庫管理過程圖的語義可以表示為

semantics(M)=□[semA(A1)∧…∧semA(A9)]

入庫業(yè)務約束規(guī)則模型包括兩條基本約束規(guī)則，如圖3所示。

規(guī)則1 的語義是執(zhí)行入庫臺賬登記之前，必須先由檢驗員簽章。用XYZ/E語言表示其語義為

□[!(LB=A22)$U(LB=A13)]

規(guī)則2 語義是執(zhí)行入庫臺賬登記之前，必須先由檢驗員進行抽檢，用XYZ/E語言表示其語義為

□[!(LB=A22)$U(LB=A12)]

6 結束語

本文提出了一種可視化的業(yè)務過程約束規(guī)則建模語言，并用時序邏輯語言XYZ/E作為邏輯框架，統(tǒng)一描述了VPML過程模型和VCML約束模型的語義，最后給出約束規(guī)則的自動驗證方法。雖然本方法選用VPML作為過程建模語言，但也適用于其他過程模型的約束驗證。接下來，將開發(fā)一種VCML可視化建模和驗證工具。該工具不僅支持業(yè)務過程約束建模和模型一致性驗證，而且當模型出現(xiàn)不一致時，應該提供一個違反約束規(guī)則的過程運行實例作為反例，幫助用戶定位模型的問題。另外，調研效率更高模型檢驗(model checking)方法，以提高所能處理的模型規(guī)模，擴大該方法的適用范圍。

參考文獻：

[1] HAMMER M， CHAMPY J. Reengineering the corporation: a manifesto for business revolution[M]. New York: Harper Business， 1993: 2-3.

[2]PERSSON A， STIRNA J. EKD user guide， IST-2000-28401[R]. Stockholm: KTH， 2000.

[3]周伯生，張社英.可視化的過程建模語言[J].軟件學報， 1997，8(增刊):535-545.

[4]王遠，范玉順.工作流時序約束模型分析與驗證方法[J].軟件學報，2007， 18(9): 2153-2161.

[5]FOERSTER A， ENGELS G， SCHATTKOWSKY T. A pattern-driven development process for quality standard-conforming business process models: visual languages and human-centric computing[M]. Brighton: IEEE Press， 2006: 135-142.

[6]唐稚松.時序邏輯程序設計與軟件工程(上、下冊)[M].北京:科學出版社， 2002.

[7]朱雪陽，唐稚松. Statecharts的組合語義與求精[J].軟件學報， 2006， 17(4): 670-681.

[8]唐稚松. XYZ系統(tǒng)的目的、意義、作用與應用[J].軟件學報， 1999， 10(4): 237-241.

[9]朱雪陽，唐稚松. UML活動圖的時序邏輯語義[J].計算機研究與發(fā)展，2005， 42(9): 1478-1484.

[10]FOERSTER A， ENGELS G， SCHATTKOWSKY T. Activity diagram patterns for modeling quality constraints in business[C]//Proc of the 8th International Conference on Model Driven Engineering Languages and Systems. Montego Bay:IEEE/ACM Press， 2006:2-16.

[11]ISO International Organization for Standardization. ISO 9001-2001， Quality management systems-requirements[S]. 2001.

[12]張莉，周伯生，崔德剛.飛機全生命期過程建模技術及支持環(huán)境[J].北京航空航天大學學報， 2001， 27(4): 417-420.

[13]譚文安，周博生，張莉.企業(yè)過程模型的柔性模擬技術研究[J].軟件學報， 2001，12(7): 1080-1087.