數(shù)據(jù)規(guī)則約束下的抽象模型一致性檢驗分析①

李 朋, 朱山川, 朱婷婷

(滁州職業(yè)技術(shù)學院，安徽 滁州 239000)

0 引 言

對于流程模型的一致性問題的研究主要有：Martens在2005年提出通過對比所提取的具體執(zhí)行的模型和抽象模型間相關(guān)信息所生成的對應(yīng)通信圖自動管理一致性的方法[4]；文獻[5]給出了一個最優(yōu)一致性關(guān)系的框架用以解決B2B流程集成場景時模型間交互的行為兼容性問題；Egyed 在2008提出了在UML中使用模型分析器監(jiān)視模型的各個部分來識別和解決不一致問題，但是該方法是半自動的[6]；此后，2010年Silva等人在文獻[6]的基礎(chǔ)上，開發(fā)了一種關(guān)于模型構(gòu)建動作序列的邏輯規(guī)則來識別模型中的不一致并且通過深度優(yōu)先搜索算法尋找最佳處理不一致方案的自動方法[7]；Weidlich 等人在2011年提出了基于模型運行期間的跡等價和所捕獲到的行為輪廓關(guān)系計算用以模型間的一致性度的測量，該方法可以計算出兩個模型之間的相似程度[8]；文獻[9]提出了一個基于節(jié)點名稱類型的算法用于建立不同抽象層次模型間的節(jié)點之間的對應(yīng)關(guān)系管理一致性；文獻[10]將基于跡等價和行為等價進行了實驗對比分析，得出基于行為等價更適合作為一致性的標準，并提出了行為一致性的概念；Grossmann等人于2015年在文獻[11]的基礎(chǔ)上提出帶標簽Petri網(wǎng)的基于規(guī)則設(shè)計的方法來檢驗不同抽象視圖模型的一致性問題[12]。目前業(yè)務(wù)流程模型研究現(xiàn)狀大多考慮的都是模型的控制流結(jié)構(gòu)方面，很少涉及數(shù)據(jù)流信息。因此，本文依據(jù)流程模型的變遷和數(shù)據(jù)之間的依賴關(guān)系，提出基于數(shù)據(jù)規(guī)則約束的抽象模型一致性檢驗分析，將業(yè)務(wù)流程轉(zhuǎn)換為基于Petri網(wǎng)的工作流系統(tǒng)，目的是實現(xiàn)控制流和數(shù)據(jù)流兩個方面的一致性檢驗。所提出的方法充分考慮了模型的數(shù)據(jù)流和控制流兩個方面，具有一定的可行性。

1 相關(guān)概念

定義1[3](工作流Petri網(wǎng))一個網(wǎng)N=(S,T;F,i,o)稱為工作流Petri網(wǎng)，當且僅當滿足條件：

(1)該Petri網(wǎng)有唯一的源庫所i:·i=φ.

(2)該Petri網(wǎng)有唯一的終止庫所o:o·=φ.

(3)該Petri網(wǎng)上的每一個節(jié)點都屬于i到o的一條路徑上,即Petri網(wǎng)是強連通的。

定義2(帶數(shù)據(jù)約束的Petri網(wǎng))一個網(wǎng)Σ=(S,T;D,F,M0,BP;DC)稱為數(shù)據(jù)流Petri網(wǎng)，當且僅當滿足條件：

(1)S為庫所集：S≠φ；

(2)T為變遷集：T≠φ；

(3)M0是初始標識，F(xiàn)是控制流關(guān)系，BP是變遷間的行為輪廓關(guān)系；

(4)D為數(shù)據(jù)集：D={d1,d2,…,dm}；

(5)DC為數(shù)據(jù)流的數(shù)據(jù)連接集：DC={dc1,dc2,…,dcm}且dc=(d,t,INP(t)/OUT(t),write/read)，其中d∈D,t∈T.INP(t)為一個輸入?yún)?shù)，OUT(t)為一個輸出參數(shù)；write為輸出數(shù)據(jù)信息的函數(shù)，即當變遷t發(fā)生時輸出數(shù)據(jù)；read為輸入數(shù)據(jù)信息的函數(shù)，即當變遷t發(fā)生時輸入數(shù)據(jù)。

本文研究抽象模型和初始模型間的一致性問題，因此下面給出初始模型和抽象模型間的一個映射函數(shù)。

h:S∪T∪D→S′∪T′∪D′∪{ξ}(h是完全的和滿射)

(1)?s∈S?h(s)∈S′∪{ξ}；

(2)?t∈T?h(t)∈T′∪{ξ}；

(3)?d∈D?h(d)∈D′∪{ξ}；

(4)s∈S,|·s|=0∧h(s)=s′?|·s′|=0；

(5)h(n)∈S∪T∪D?h(n)=n；

(6)h(n1)=n′∧h(n2)=n′?n1=n2；

其中性質(zhì)(1)保證Σ中的庫所被映射為Σ′中的一個庫所或者被刪除；性質(zhì)(2)保證Σ中的變遷被映射為Σ′中的一個變遷或者被刪除；性質(zhì)(3)保證Σ中的數(shù)據(jù)被映射為Σ′中的一個數(shù)據(jù)或者被刪除；性質(zhì)(4)保證Σ中的源庫所被映射為Σ′中的源庫所；性質(zhì)(5)保證被映射到Σ′中的一個節(jié)點(庫所、變遷和數(shù)據(jù))如果屬于Σ中的節(jié)點，則在抽象過程中該節(jié)點未發(fā)生變化；性質(zhì)(6)保證Σ中有且僅有唯一的一個節(jié)點與Σ′中的節(jié)點相對應(yīng)。模型的抽象涉及三個基本操作：節(jié)點不變、節(jié)點聚合和節(jié)點刪除。當節(jié)點保持不變時，有h(n)=n；當節(jié)點n1,n2,n3被聚合成一個節(jié)點n′時，有h({n1,n2,n3})=n′；當節(jié)點被刪除時，有h(n)=ξ。

下面給出上述定義的具體例子，如圖1所示的帶數(shù)據(jù)流的Petri業(yè)務(wù)流程模型，其中d1,d2為模型中的數(shù)據(jù)元素，實線箭頭代表的是變遷之間的控制流關(guān)系，虛線箭頭代表了變遷之間的數(shù)據(jù)連接。1)模型的控制流結(jié)構(gòu)：由BP定義可知，變遷t2,t5為并發(fā)序關(guān)系，記為t2‖t5；t3,t4為排他序關(guān)系，記為t3+t4；t1,t7為嚴格序，記為t1→t7；2)模型的數(shù)據(jù)流結(jié)構(gòu)：如變遷t1發(fā)生要將數(shù)據(jù)d1發(fā)送給變遷t2，根據(jù)定義3可知，此時變遷t1的數(shù)據(jù)連接為dc1=(d1,t1,OUT(t1),write)。而當變遷t1發(fā)生后通過庫所s1導致變遷t2發(fā)生，此時數(shù)據(jù)d1被變遷t2連接，因此變遷t2的數(shù)據(jù)連接為dc2=(d1,t2,INP(t2),read)。

現(xiàn)在對圖1的模型進行抽象化簡，現(xiàn)假設(shè)給定一個指定的抽象條件，需要將模型中的變遷t3,t4進行聚合操作，變遷t2進行刪除操作，其他的保持不變，則由分析可知，t2接收來自t1發(fā)送的數(shù)據(jù)信息d1，現(xiàn)t2進行刪除操作，因此，d1也將被刪除，則有h({t3,t4})=X,h(t2)=ξ，h(d1)=ξ，h(ti)=ti(i≠2，3，4)，h(d2)=d2，h(sj)=sj(j≠2,3)，抽象后的模型Σ′如圖2所示。

圖1 帶數(shù)據(jù)流的Petri業(yè)務(wù)流程模型Σ

圖2 圖1的抽象模型Σ'

根據(jù)不同利益相關(guān)者指定的抽象條件，將初始模型進行不同的抽象化簡，則需要對抽象模型和初始模型進行一致性檢驗分析，檢查抽象模型的一致性和非一致性。下面給出具體的基于控制流和數(shù)據(jù)流的抽象模型的一致性檢驗規(guī)則。

2 一致性檢驗規(guī)則

現(xiàn)有關(guān)于一致性問題的研究主要針對流程模型的控制流結(jié)構(gòu)，本文延伸了先前的工作，不僅包括控制流還包括數(shù)據(jù)流方面，下面先給出抽象模型的控制流的一致性檢驗規(guī)則，其次再給出數(shù)據(jù)流的一致性檢驗規(guī)則。

2.1 控制流的一致性檢驗標準

(1)規(guī)則2.1.1 變遷不變的前集和后繼滿足：

a)?s1∈S,t1∈T:

h(s1)=s1∧h(t1)=t1∧(s1,t1)∈F′?(s1,t1)∈F

b)?s1∈S,t1∈T:

h(s1)=s1∧h(t1)=t1∧(t1,s1)∈F′?(t1,s1)∈F

規(guī)則2.1.1針對的是抽象操作前后不變的變遷前集和后繼滿足情況，該規(guī)則保證了抽象模型視圖中未發(fā)生改變的流關(guān)系需要被反映在初始模型中對應(yīng)的流關(guān)系。

(2)規(guī)則2.1.2 變遷刪除的前集和后繼滿足：

a) ?s1∈S,t1∈T:

h(t1)=ξ∧(s1,t1)∈F?h(s1)=

ξ∧(h(s1),h(t1))=ξ

b)?s1∈S,t1∈T:

h(t1)=ξ∧(t1,s1)∈F?h(s1)=

ξ∧(h(t1),h(s1))=ξ

規(guī)則2.1.2針對的是抽象操作前后被刪除變遷的前集和后繼滿足情況，該規(guī)則保證了流程模型在抽象過程中，如果一個變遷被刪除操作，則抽象模型視圖中該變遷的前后庫所以及對應(yīng)的流關(guān)系都應(yīng)被刪除。

圖3描述了一個初始模型a給定將變遷t2刪除操作，根據(jù)規(guī)則2.1.2需要同時將t2的前后庫所s1,s2都刪除，抽象后的視圖如b所示。

圖3 規(guī)則2.1.2案例模型

(3)規(guī)則2.1.3 變遷聚合的前集和后繼滿足：

b)?t1,t2,…,tm∈T,s1∈S,s1′,s2′∈S′,t′∈T′:

規(guī)則2.1.1針對抽象操作前后被聚合變遷的前集和后繼滿足情況，該規(guī)則驗證了在抽象模型視圖中的行為關(guān)系要被正確反映在初始模型中，該規(guī)則約束保證了初始模型和抽象模型視圖之間流關(guān)系彼此的一致性。

圖4描述了一個初始模型a給定將變遷t1,t2,t3聚合操作，由于變遷t2有一個前集庫所s5且該庫所不包含在被聚合操作里，根據(jù)規(guī)則2.1.3，s5與被聚合后的變遷的行為關(guān)系應(yīng)該被保留，抽象后的視圖如b所示。

圖4 規(guī)則2.1.3案例模型

2.2 數(shù)據(jù)流的一致性檢驗標準

在2.1部分已經(jīng)介紹了控制流的一致性檢驗標準，現(xiàn)在來介紹對應(yīng)的數(shù)據(jù)流的一致性檢驗標準。本文定義了兩種類型關(guān)于流程模型數(shù)據(jù)流的抽象操作，即概括(generalization)和刪除(deletion)。其中，概括是指對于那些在抽象過程中作為數(shù)據(jù)輸入對象的且不發(fā)生改變的變遷，其數(shù)據(jù)在抽象過程中保持不變；對于那些在抽象過程中作為數(shù)據(jù)輸入對象且被認為是不重要的被刪除的變遷，或者作為數(shù)據(jù)輸入和輸出的變遷包含在一組被抽象的變遷序列中，則其數(shù)據(jù)在抽象過程中被刪除。

(1)規(guī)則2.2.1 數(shù)據(jù)不變時滿足

a) ?t1,t2∈T,d∈D:

h(t1)=t1∧h(t2)=t2∧t1→dt2?h(d)=d

b1) ?t′,ti′∈T′,t1,…,tm∈T,d∈D:

??ti∈TR(t′):h(ti)=ti′∧ti→dtj(tj∈R(t′))

b2) ?t′,ti′∈T′,t1,…,tm∈T,d∈D:

h({t1,…,tm})=t′∧h(d)=d∧t′→dti′

??ti∈TR(t′):h(ti)=ti′∧tj→dti(tj∈R(t′))

c) ?t1,t2∈T,d∈D:

h(d)=d∧t1→dt2∧h(t2)≠ξ?h(t1)≠ξ

規(guī)則2.2.1針對，規(guī)則a)檢查了如果抽象過程中初始模型中的兩個變遷不發(fā)生變化，則兩個變遷之間的數(shù)據(jù)連接也應(yīng)該被放映到抽象模型視圖中對應(yīng)變遷中；b1),b2)檢查了抽象模型視圖中被聚合后變遷的數(shù)據(jù)輸入和輸出都應(yīng)該被反映在初始模型中該變遷的域所包含的組件中；c)檢查了作為數(shù)據(jù)輸入對象的變遷如果在抽象過程中不被刪除，則作為數(shù)據(jù)輸出的變遷在抽象過程中也應(yīng)該被保留，規(guī)則2.2.1保證了抽象過程中初始模型和抽象模型視圖之間數(shù)據(jù)不變的一致性。

圖5 規(guī)則2.2.1案例模型

圖6 規(guī)則2.2.2案例模型

圖5描述了一個初始模型a給定將變遷t1,t2,t3聚合操作，由于變遷t2有一個輸入數(shù)據(jù)d且d的輸出變遷t4不包含在被聚合操作里，根據(jù)規(guī)則3.2.1，數(shù)據(jù)d應(yīng)該被保留，抽象后的視圖如b所示。

(2)規(guī)則2.2.2 數(shù)據(jù)被刪除時滿足

a) ?t1,t2∈T,d∈D:t1→dt2∧h(t2)=

ξ∧(??t3∈T:t1→dt3∧h(t3)≠ξ)?h(d)=ξ

b) ?t1,t2,…,tm∈T,d∈D,t′∈T:

h({t1,…,tm})=t′∧ti→dtj?h(d)=

ξ(ti,tj∈R(t′))

規(guī)則2.2.2針對的是抽象操作前后數(shù)據(jù)被刪除時的滿足情況，規(guī)則a)檢查了如果在抽象過程中，某個數(shù)據(jù)被刪除當且僅當該數(shù)據(jù)的輸入對象被刪除且沒有另一個變遷作為此數(shù)據(jù)的輸入對象時，則在抽象視圖中該數(shù)據(jù)被刪除;規(guī)則b)檢查了包含在一組被抽象變遷序列中的變遷之間的數(shù)據(jù)輸入和輸出應(yīng)該被刪除。

圖6描述了一個初始模型a給定將變遷t1,t2,t3聚合操作，由于變遷t1,t2之間有一個輸入數(shù)據(jù)d且d包含在被聚合操作的域中，根據(jù)規(guī)則3.2.1，數(shù)據(jù)d應(yīng)該被隱藏(刪除)，抽象后的視圖如b所示。

3 結(jié) 論

本文基于Petri網(wǎng)的工作流系統(tǒng)，提出基于控制流和數(shù)據(jù)流兩個方面的抽象模型一致性檢驗規(guī)則，并且通過實例驗證了該方法的有效性和可行性,未來可以進一步針對大型的較復雜的業(yè)務(wù)流程系統(tǒng)的抽象檢驗規(guī)則進行探究。