業(yè)務(wù)協(xié)同中組織需求的建模與一致性驗(yàn)證

笪 建，莫 啟，程耀坤,張 毅，李 彤

(1.云南大學(xué) 軟件學(xué)院，云南 昆明 650091；2.云南大學(xué) 云南省軟件工程重點(diǎn)實(shí)驗(yàn)室，云南 昆明 650091；3.淮安開放大學(xué) 信息工程系，江蘇，淮安 223001;4.江蘇聯(lián)合職業(yè)技術(shù)學(xué)院淮安分院 現(xiàn)代教育技術(shù)中心 223001)

0 引言

隨著全球經(jīng)濟(jì)化的發(fā)展和企業(yè)信息化程度的不斷提高，企業(yè)的經(jīng)營模式發(fā)生了重大變化，企業(yè)的業(yè)務(wù)活動已從企業(yè)內(nèi)單目標(biāo)為導(dǎo)向的獨(dú)立發(fā)展模式發(fā)展成為跨企業(yè)多目標(biāo)合作的協(xié)同模式[1]。在現(xiàn)代商業(yè)環(huán)境下，沒有一個企業(yè)是孤立的[2-3]。企業(yè)作為參與者參與到協(xié)作中，在協(xié)作過程中，它們彼此進(jìn)行交互以完成特定業(yè)務(wù)功能。近年來，隨著互聯(lián)網(wǎng)成為主流的計算平臺，尤其是面向服務(wù)計算(Service-Oriented Computing, SOC)的快速興起，使得不同組織業(yè)務(wù)過程間的交互成為可能，如企業(yè)信息系統(tǒng)[4]、電子商務(wù)[5]等。為實(shí)現(xiàn)共同的商業(yè)目標(biāo)，每個組織的業(yè)務(wù)過程通常需要跨越組織邊界，同其他組織的業(yè)務(wù)過程進(jìn)行交互和協(xié)作，以形成相對穩(wěn)定的過程視圖。學(xué)術(shù)界和工業(yè)界稱這種存在復(fù)雜交互和協(xié)作關(guān)系的業(yè)務(wù)過程為協(xié)同業(yè)務(wù)過程[6]。為確保協(xié)同業(yè)務(wù)過程實(shí)施的正確性，在設(shè)計階段對協(xié)同業(yè)務(wù)過程進(jìn)行建模與驗(yàn)證是當(dāng)前業(yè)務(wù)過程管理(Business Process Management, BPM)領(lǐng)域研究的熱點(diǎn)。

針對協(xié)同業(yè)務(wù)過程，已有研究工作大多圍繞如何構(gòu)建支持個性化特征的協(xié)同業(yè)務(wù)過程開展，如文獻(xiàn)[7-8]，并以此為基礎(chǔ)對相關(guān)性質(zhì)(如弱合理性等)進(jìn)行驗(yàn)證，如文獻(xiàn)[9]。而事實(shí)上，衡量協(xié)同業(yè)務(wù)過程質(zhì)量的因素除了模型本身無歧義、一致性和無錯誤等性質(zhì)外，更重要的是其能否充分滿足參與組織需求。一些研究者注意到了上述問題，并基于目標(biāo)模型提出了業(yè)務(wù)過程需求一致性驗(yàn)證方法，如文獻(xiàn)[10]，但這些方法僅針對單個業(yè)務(wù)流程。協(xié)同業(yè)務(wù)過程中含有多個參與組織流程，這些流程間相互通信合作，共同推進(jìn)全局流程演進(jìn)[11]。由于上述方法沒有考慮多流程間協(xié)作的情形，很難應(yīng)用于跨組織環(huán)境下的需求一致性驗(yàn)證。解決協(xié)同業(yè)務(wù)過程需求一致性問題面臨以下挑戰(zhàn)：①如何準(zhǔn)確地描述跨組織環(huán)境下的需求；②如何形式化建模支持需求分析的協(xié)同業(yè)務(wù)過程；③如何驗(yàn)證協(xié)同業(yè)務(wù)過程與需求保持一致。

本文借鑒經(jīng)典需求工程中目標(biāo)模型[12]的思想，并基于模型檢測技術(shù)提出一種驗(yàn)證協(xié)同業(yè)務(wù)過程與參與組織需求一致性的方法。該方法將參與組織需求以類似目標(biāo)模型方式構(gòu)建，并將其和協(xié)同業(yè)務(wù)過程分別轉(zhuǎn)化為以線性時序邏輯公式(Linear Temporal Logic, LTL)描述性質(zhì)和可形式驗(yàn)證的模型，借助模型檢測技術(shù)實(shí)現(xiàn)需求一致性自動驗(yàn)證。

本文主要貢獻(xiàn)如下：

(1)借鑒經(jīng)典需求工程中目標(biāo)模型思想，提出了需求依賴圖(Requirement Dependence Graph, RDG)來顯式刻畫參與組織需求間依賴關(guān)系，通過分析協(xié)同業(yè)務(wù)過程特性[11]給出跨組織環(huán)境下原子需求定義。

(2)采用Petri網(wǎng)建模參與組織業(yè)務(wù)過程，引入并發(fā)操作符提供一種通過組合參與組織業(yè)務(wù)過程構(gòu)建協(xié)同業(yè)務(wù)過程的方法。提出需求產(chǎn)生式用來刻畫需求隨任務(wù)執(zhí)行產(chǎn)生規(guī)則。在明確需求產(chǎn)生規(guī)則前提下，以任務(wù)執(zhí)行為驅(qū)動提出了協(xié)同業(yè)務(wù)過程執(zhí)行語義，以支持需求一致性驗(yàn)證。

(3)基于模型檢測技術(shù)提出需求一致性驗(yàn)證框架。從跡等價[13]角度證明了協(xié)同業(yè)務(wù)過程與轉(zhuǎn)換生成NuSMV規(guī)約間在參與組織需求層面具有一致檢測結(jié)果，并給出將參與組織需求自動轉(zhuǎn)換成LTL公式的算法。以此為基礎(chǔ)借助NuSMV實(shí)現(xiàn)了參與組織需求自動驗(yàn)證。

(4)結(jié)果表明，相對已有工作，本文方法不僅可直接應(yīng)用于建模跨組織需求和支持需求分析過程模型，還可更加有效地刻畫參與組織需求和驗(yàn)證需求一致性。

1 相關(guān)研究

目前國內(nèi)外研究者就協(xié)同業(yè)務(wù)過程建模與驗(yàn)證開展了一系列相關(guān)工作。

在協(xié)同業(yè)務(wù)過程建模方面，文獻(xiàn)[14]將Petri網(wǎng)和Pi演算交叉應(yīng)用，提出一種協(xié)同業(yè)務(wù)過程的建模方法以支持協(xié)同業(yè)務(wù)過程具有面向流程組合的特性。為了保護(hù)參與組織內(nèi)部流程信息，文獻(xiàn)[8]首先提出一組元結(jié)構(gòu)，然后針對每種元結(jié)構(gòu)提出各自的約簡規(guī)則，得到參與組織的公共視圖，將公共視圖進(jìn)行組合從而得到跨組織協(xié)同的信息流網(wǎng)結(jié)構(gòu)，即協(xié)同業(yè)務(wù)過程。文獻(xiàn)[15]基于Petri網(wǎng)提出一種多視角的跨組織業(yè)務(wù)過程建模方法。該方法從內(nèi)部視角定義私有過程，進(jìn)而通過抽取規(guī)則集生成公共過程，將公共過程組合生成協(xié)作過程。文獻(xiàn)[16]引入了過程視圖概念，過程視圖由投影規(guī)則(如灰盒投影、白盒投影等)從私有過程中生成，它隱藏了私有業(yè)務(wù)過程中無關(guān)的信息，僅暴露相關(guān)協(xié)作信息，可視為私有過程的外部映像。進(jìn)而通過將過程視圖組合得到協(xié)同業(yè)務(wù)過程。然而，這些研究工作關(guān)注的重點(diǎn)是如何構(gòu)建支持個性化特征[11](如面向流程組合、隱私等)的協(xié)同業(yè)務(wù)過程模型，沒有討論協(xié)同業(yè)務(wù)過程驗(yàn)證。

在協(xié)同業(yè)務(wù)過程形式驗(yàn)證中，文獻(xiàn)[7]較早在國際上提出了跨組織工作流網(wǎng)(Inter-Organizational WorkFlow, IOWF)用于建?？缃M織工作流，并基于傳統(tǒng)的合理性定義了IOWF的正確性。在此基礎(chǔ)上，國內(nèi)外研究者開展了相關(guān)研究。文獻(xiàn)[17]采用Petri網(wǎng)和Pi演算分別對協(xié)同業(yè)務(wù)過程的本地控制流及控制流間交互協(xié)議進(jìn)行建模，并基于Petri網(wǎng)可達(dá)圖建立了本地控制流和交互協(xié)議間的關(guān)聯(lián)關(guān)系；然后，定義了協(xié)同業(yè)務(wù)過程邏輯結(jié)構(gòu)的正確性，進(jìn)而提出了邏輯結(jié)構(gòu)正確性驗(yàn)證方法。為了避免形式驗(yàn)證中狀態(tài)空間爆炸問題，文獻(xiàn)[9]提出一種協(xié)同業(yè)務(wù)過程模型，即利用面向交互的Petri網(wǎng)(Interaction-Oriented Petri Nets, IOPN)用于描述參與組織間業(yè)務(wù)協(xié)同；然后，引入IOPN弱合理性概念用來定義IOPN的邏輯結(jié)構(gòu)正確性，并基于不變量分解方法將一個弱合理的無回路IOPN分解為一組順序圖用于驗(yàn)證其邏輯結(jié)構(gòu)正確性。文獻(xiàn)[6]針對跨部門業(yè)務(wù)協(xié)同呈現(xiàn)出的復(fù)雜特性，對WF-net擴(kuò)展資源和消息等要素來建模參與部門的業(yè)務(wù)流程，然后使用庫所融合技術(shù)將資源庫所和消息庫所融合以得到跨部門協(xié)調(diào)業(yè)務(wù)過程模型。以傳統(tǒng)合理性為基礎(chǔ)定義了協(xié)調(diào)業(yè)務(wù)過程模型正確性標(biāo)準(zhǔn)，并基于可達(dá)圖給出協(xié)同業(yè)務(wù)過程正確性分析方法。為了有效地存儲和描述互操作需求，文獻(xiàn)[18]首先提出一種領(lǐng)域描述語言用來描述互操作需求，繼而將描述需求自動轉(zhuǎn)換為時間計算樹邏輯(Time Computation Tree Logic, TCTL)，并采用時間自動機(jī)網(wǎng)絡(luò)(Timed Automata Network, TAN)建模協(xié)同業(yè)務(wù)過程。通過UPPAAL實(shí)現(xiàn)互操作需求的自動驗(yàn)證。然而，以上工作重點(diǎn)關(guān)注協(xié)同業(yè)務(wù)過程邏輯結(jié)構(gòu)正確性或互操作方面需求，并未考慮參與組織共性及個性需求這一重要因素。

為此，國內(nèi)外研究者提出了一些關(guān)于需求形式驗(yàn)證的方法。為支持用戶需求意圖表達(dá)，文獻(xiàn)[19]提出一種基于目標(biāo)感知的可配置業(yè)務(wù)流程分析方法。該方法將用戶需求與業(yè)務(wù)過程進(jìn)行融合，進(jìn)而通過增加配置操作將用目標(biāo)工作流網(wǎng)(Goal WF-net, GWF-net)表達(dá)的業(yè)務(wù)過程轉(zhuǎn)化為符合用戶個性化需求的流程模型。為確保業(yè)務(wù)過程滿足用戶特定需求，文獻(xiàn)[10]提出一種目標(biāo)模型與過程模型一致性驗(yàn)證方法。該方法采用目標(biāo)模型對用戶需求進(jìn)行建模，PZN(Z+Petri Net)模型用于刻畫業(yè)務(wù)過程，繼而基于PZN模型活動路徑來驗(yàn)證是否滿足目標(biāo)模型。盡管文獻(xiàn)[10]和文獻(xiàn)[19]對用戶需求與業(yè)務(wù)過程模型一致性問題進(jìn)行了討論，但這些工作僅局限于組織內(nèi)單個業(yè)務(wù)過程，未涉及業(yè)務(wù)過程間協(xié)作，不適用于跨組織環(huán)境下需求一致性驗(yàn)證。考慮到目標(biāo)能夠良好地反映參與組織需求意圖，文獻(xiàn)[20]基于面向目標(biāo)業(yè)務(wù)過程提出一種分布式的協(xié)同業(yè)務(wù)過程監(jiān)控與管理方法。該方法通過實(shí)時收集業(yè)務(wù)過程中任務(wù)執(zhí)行的相關(guān)目標(biāo)信息實(shí)現(xiàn)挖掘分析。盡管文獻(xiàn)[20]闡述了利用目標(biāo)進(jìn)行協(xié)同業(yè)務(wù)過程建模、分析及監(jiān)控的重要性，但對于如何驗(yàn)證協(xié)同業(yè)務(wù)過程與需求的一致性沒有進(jìn)行討論。

2 組織需求和協(xié)同業(yè)務(wù)過程建模

本章對參與組織需求和協(xié)同業(yè)務(wù)過程的建模方法進(jìn)行詳細(xì)闡述。

2.1 需求依賴圖RDG

傳統(tǒng)目標(biāo)模型能夠良好地描述需求間存在的例化和分解關(guān)系[12]。通過擴(kuò)展目標(biāo)模型，本文提出需求依賴圖RDG來描述參與組織期望需求。在RDG中，根據(jù)構(gòu)建參與組織需求的需要，增加Pre依賴來表達(dá)需求間存在的時序關(guān)系，同時添加XOR依賴來進(jìn)一步表示現(xiàn)實(shí)中需求間存在的互斥關(guān)系。在RDG中，需求可分為原子需求和組合需求兩類，原子需求是建模參與組織需求的最小粒度，而組合需求通?？煞纸鉃橐唤M原子需求集合。

特別地，RDG中需求之間存在的依賴關(guān)系可從垂直和水平兩個角度區(qū)分：①從垂直視角，需求之間的依賴關(guān)系可分為與分解關(guān)系和或分解關(guān)系，用于將高層次需求(即概念需求)逐層細(xì)化成低層次需求(其中最底層需求是消息，表示實(shí)際交互行為)，為參與組織提供一種逐層細(xì)化其意圖方法，降低建模復(fù)雜性；②從水平視角，需求之間的依賴關(guān)系可分為前驅(qū)關(guān)系和互斥關(guān)系，分別用于描述協(xié)同業(yè)務(wù)過程中交互發(fā)生的先后關(guān)系和互斥關(guān)系。例如，在京東或蘇寧網(wǎng)購中，店主通常要求客戶先付款后發(fā)貨。如果缺少前驅(qū)關(guān)系Pre，則參與組織就不能表達(dá)出這種訴求。同時，客戶在支付過程中只能使用一種支付方式(如支付寶、微信及網(wǎng)銀等)，因此利用互斥關(guān)系就能夠描述出客戶支付方式互斥需求。RDG的形式定義如下。

定義1RDG是一個3元組G=(V,E,φ)，其中：

(1)V為節(jié)點(diǎn)有限集合，表示參與組織需求集合。

(2)E:V×V為節(jié)點(diǎn)間存在有向邊集。

(3)標(biāo)注函數(shù)φ:E×{AND,OR,XOR,Pre}用來標(biāo)識有向邊類型，這些類型包括與分解關(guān)系(AND)、或分解關(guān)系(OR)、異或分解關(guān)系(XOR)和前驅(qū)關(guān)系(Pre)。

定義1中，RDG中每個節(jié)點(diǎn)表示一個需求。原子需求在V中映射為葉子節(jié)點(diǎn)(原子需求定義參見定義3)，而組合需求對應(yīng)非葉子節(jié)點(diǎn)，它由原子需求或低層次組合需求通過分解關(guān)系構(gòu)成；節(jié)點(diǎn)間有向邊表示需求間存在依賴關(guān)系；邊上的標(biāo)記為依賴關(guān)系類型。為了方便表述需求間依賴關(guān)系，若需求R由{R1,…,Rn}通過AND分解組成，則記為R=R1&…&Rn，表示當(dāng)R1,…,Rn全部完成時R才能完成；若需求R由{R1,…,Rn}通過OR分解組成，則記為R=R1‖…‖Rn，表示當(dāng)R1,…,Rn中有一個或多個完成時R才能完成；若需求Ri，Rj滿足Pre關(guān)系，則記為Ri→Rj，表示當(dāng)Rj完成時Ri已經(jīng)完成；若需求Ri，Rj滿足XOR關(guān)系，則記為Ri?Rj，表示Ri和Rj間是異或關(guān)系，即兩者只能取其一。

進(jìn)一步以G為基礎(chǔ)，參與組織需求良構(gòu)性定義如下。

定義2參與組織需求良構(gòu)性。當(dāng)且僅當(dāng)R對應(yīng)的需求依賴圖G=(V,E,φ)滿足如下條件，稱參與組織需求R具有良構(gòu)性：

(1)存在唯一根需求root，滿足對于?v∈V，(v,root)?V。

(2)對于?vi∈V，若ei1=(vi,vi1),…,ein=(vi,vin)∈E且φ(eij)∈{AND,OR}，則φ(ei1)=…=φ(ein)。

(3)若?e=(vi,vj)∈E且φ(e)=Pre，則?v∈V，ei=(v,vi)，ej=(v,vj)∈E，使得φ(ei)=φ(ej)=AND。

(4)若?e=(vi,vj)∈E且φ(e)=XOR，則?v∈V，ei=(v,vi)，ej=(v,vj)∈E，使得φ(ei)=φ(ej)=OR。

(5)G不存在環(huán)結(jié)構(gòu)。

定義2中，條件(2)要求每次分解類型必須相同；條件(3)要求前驅(qū)關(guān)系只能指定由與分解得到的同一層次上不同需求執(zhí)行先后關(guān)系；條件(4)要求互斥關(guān)系只能指定由與分解得到的同一層次上不同需求執(zhí)行互斥關(guān)系；條件(5)要求G中不存在環(huán)結(jié)構(gòu)，避免出現(xiàn)循環(huán)分解和循環(huán)前驅(qū)。

其中：條件(2)和條件(5)與經(jīng)典需求模型保持一致[12]；條件(3)和條件(4)是受到文獻(xiàn)[21]啟發(fā)提出，即文獻(xiàn)[21]認(rèn)為在實(shí)際建模中約束關(guān)系(即Pre關(guān)系和XOR關(guān)系)主要定義在同一層次。同時，也方便后文將以RDG描述需求轉(zhuǎn)換為LTL公式。在實(shí)際應(yīng)用中，約束關(guān)系也可能分布在RDG中的不同層次，這將在下一步工作中詳細(xì)討論。

在實(shí)際應(yīng)用中，參與組織需求通常由協(xié)同業(yè)務(wù)過程執(zhí)行情況確定。以參與組織內(nèi)部任務(wù)執(zhí)行為驅(qū)動，協(xié)同業(yè)務(wù)過程行為在參與組織間表現(xiàn)為消息傳遞[11]。此外，跨組織環(huán)境下消息傳遞具有異步特性，使得在協(xié)作中產(chǎn)生多種消息狀態(tài)。一條消息及其在某個時刻所處狀態(tài)是參與組織觀察協(xié)同業(yè)務(wù)過程執(zhí)行情況的最小粒度。為此本文將消息及其狀態(tài)進(jìn)行組合來表示原子需求。

由于原子需求中涉及消息狀態(tài)，本文通過對任務(wù)與消息交互過程進(jìn)行分析，將消息狀態(tài)進(jìn)行統(tǒng)一抽象，如圖1所示。

對于任意消息(message)，開始時其處于未生成狀態(tài)(inactive)；在任務(wù)task(任務(wù)定義參見定義2)執(zhí)行完成并發(fā)送消息message后(消息生成由任務(wù)內(nèi)部執(zhí)行確定，任務(wù)執(zhí)行在本文中認(rèn)為是原子的，故產(chǎn)生狀態(tài)沒有顯示列出)，其處于投遞狀態(tài)(delivered)；之后若message沒有被接收則將處于等待接收狀態(tài)(pending)；一旦message被接收則將處于接收狀態(tài)(received)。

本文默認(rèn)協(xié)同業(yè)務(wù)過程執(zhí)行處于一個足夠良好的通信環(huán)境中，即若一個參與組織發(fā)生一條消息，則請求該消息的組織一定可以在規(guī)定時間內(nèi)被接受，不存在消息有效性時長問題。這種假設(shè)在協(xié)同業(yè)務(wù)過程的形式驗(yàn)證中是合理的[22]。

在明確消息狀態(tài)的前提下，將原子需求定義如下。

定義3原子需求是2元組atomic=(msg,state)，其中：

(1)msg為消息。

(2)state∈{inactive,delivered,pending,received}為消息所處狀態(tài)。

在實(shí)際應(yīng)用中，參與組織的需求由組織間協(xié)商得到，進(jìn)而可采用RDG進(jìn)行描述。特別地，需求獲取是一個循環(huán)迭代的過程，如何迭代求精獲取需求可參考文獻(xiàn)[23]。限于篇幅，本文后續(xù)討論中的需求均指經(jīng)反復(fù)協(xié)商得到的最終需求。

在跨組織環(huán)境下，參與組織需求可能有天然的不一致性，通?？煞譃樾枨笕哂嗪托枨鬀_突兩類[24]。前者是指存在一個需求，該需求可由其他需求推出，對這種需求進(jìn)行分析沒有必要，而后者則是指針對兩種需求，協(xié)同業(yè)務(wù)過程無法同時滿足，導(dǎo)致對其分析是徒勞的。文獻(xiàn)[24]對如何消除這兩類需求不一致性進(jìn)行了較為詳細(xì)的討論。限于篇幅，本文后續(xù)討論中的需求均指無冗余和無沖突的需求。此外，文獻(xiàn)[23]也認(rèn)為需求不一致性并不限于需求冗余和需求沖突兩類。由于本文主要關(guān)注需求定義及需求與模型一致性分析，如何進(jìn)一步消除需求間存在的不一致性將在進(jìn)一步的工作中詳細(xì)討論。

2.2 協(xié)同業(yè)務(wù)過程

業(yè)務(wù)過程是參與組織流程信息的本地定義，由該組織自治管理。業(yè)務(wù)過程由參與組織任務(wù)集和建立其上的控制流組成，是構(gòu)建協(xié)同業(yè)務(wù)過程的基礎(chǔ)。

任務(wù)是組織為完成特定業(yè)務(wù)目標(biāo)開展的業(yè)務(wù)活動，其形式定義如下。

(1)name是任務(wù)名字，唯一標(biāo)識組織內(nèi)一個任務(wù)。

(2)org是任務(wù)所屬的組織。

(3)MsgRec是任務(wù)執(zhí)行前需接收的消息集合。

(4)MsgSend是任務(wù)執(zhí)行完成后發(fā)送消息集合。

對于任意任務(wù)task，task.MsgRec為task接收消息集合；task.MsgSend為task發(fā)送消息集合。

本文采用Petri網(wǎng)對業(yè)務(wù)過程控制流進(jìn)行建模。進(jìn)一步地，將以Petri網(wǎng)建?？刂屏髦忻總€變遷關(guān)聯(lián)一個任務(wù)從而得到業(yè)務(wù)過程。有關(guān)Petri網(wǎng)詳細(xì)內(nèi)容參見文獻(xiàn)[25]。業(yè)務(wù)過程形式定義如下。

定義5業(yè)務(wù)過程是一個三元組BP=(Tasks,Flow,f)，其中：

(1)Tasks是有限任務(wù)集，對于?task∈Tasks，task是符合定義4的任務(wù)。

(2)Flow為控制流，它是一個基本Petri網(wǎng)Flow=(P,T;F,M0,i,o)，其中：P是有限庫所集；T是有限變遷集；F?(P×T)∪(T×P)是流關(guān)系；M0是初始標(biāo)識，滿足?p∈P，p≠i：M0(p)=0且M0(i)=1；i和o是兩個特殊庫所，分別表示開始庫所和終止庫所。

在平時的教學(xué)中，我們要培養(yǎng)勤于思考的良好習(xí)慣，對人對事都要有自己的見解。譬如，在指導(dǎo)學(xué)生寫一篇關(guān)于“門”的話題作文時，我們可引導(dǎo)他們進(jìn)行思維發(fā)散?？蓪懹行蔚拈T，如家門、校門、城門等；也可寫無形的門，如科學(xué)之門、心靈之門等；可寫門內(nèi)的世界，也可寫門外的世界；可寫開門的意義，也可寫關(guān)門的意義；可從身邊的小事引發(fā)對“門”的感受與收獲，可以由“門”聯(lián)系歷史事實(shí)去發(fā)表看法，也可以由“門”的自然屬性闡發(fā)哲理。我們還可以引導(dǎo)學(xué)生大膽指點(diǎn)教材，激揚(yáng)文字，增加自信。教師不妨開幾節(jié)欣賞課，采用逆向教學(xué)，讓學(xué)生開懷評點(diǎn)教材中的不足之處，或主題，或構(gòu)思，或語言，或邏輯，每人講那么一兩點(diǎn)，并敢于對名家名篇“開刀”。

(3)f:T→Tasks是變遷映射函數(shù)，表示每個變遷關(guān)聯(lián)一個任務(wù)。

以業(yè)務(wù)過程為基礎(chǔ)可定義協(xié)同業(yè)務(wù)過程。由于進(jìn)程代數(shù)能夠自然地以模塊的方式構(gòu)建復(fù)雜的交互并發(fā)系統(tǒng)[26]，借鑒其思想，本文引入并發(fā)操作符的概念，并發(fā)操作符提供一種通過組合參與組織業(yè)務(wù)過程構(gòu)建協(xié)同業(yè)務(wù)過程方法。

定義6協(xié)同業(yè)務(wù)過程。設(shè)參與協(xié)同的業(yè)務(wù)過程為BP1,…,BPn，由這n個業(yè)務(wù)過程構(gòu)成的協(xié)同業(yè)務(wù)過程記為CBP=BP1‖…‖BPn。

定義6只是將多個業(yè)務(wù)流程在形式上列為并發(fā)關(guān)系，其間存在協(xié)作關(guān)系，可按實(shí)際場景定義。本文僅考慮業(yè)務(wù)過程中存在的異步消息通信關(guān)系(參見定義10)。實(shí)際中，業(yè)務(wù)過程中可能還存在同步等情形，即一個協(xié)作實(shí)現(xiàn)需要多個任務(wù)同時參與完成，這將在后續(xù)工作中進(jìn)行詳細(xì)討論。

本文引入格局的概念來表示協(xié)同業(yè)務(wù)過程狀態(tài)，它由每個參與組織運(yùn)行狀態(tài)及協(xié)作中產(chǎn)生消息組成，其形式定義如下。

(2)MS為消息狀態(tài)，即c中當(dāng)前含有消息集合。

對于任意格局r，r[i]為格局中業(yè)務(wù)過程BPi的運(yùn)行狀態(tài)，r.MS為r當(dāng)前含有消息集。

可對格局運(yùn)行狀態(tài)或消息進(jìn)行替換，格局運(yùn)行狀態(tài)替換和格局信息替換定義如下。

定義協(xié)同業(yè)務(wù)過程語法規(guī)則之后，對協(xié)同業(yè)務(wù)過程執(zhí)行語義進(jìn)行討論。

本質(zhì)上，協(xié)同業(yè)務(wù)過程執(zhí)行語義刻畫由任務(wù)執(zhí)行引起的格局轉(zhuǎn)換的過程。為支持需求一致性驗(yàn)證，執(zhí)行語義中還需考慮參與組織需求。結(jié)合圖1所示的消息狀態(tài)抽象和任務(wù)定義，本文引入需求產(chǎn)生式概念來刻畫參與組織需求隨任務(wù)執(zhí)行產(chǎn)生規(guī)則。需求產(chǎn)生式如表1所示。

表1 需求產(chǎn)生式

表中：規(guī)則R1是指若存在需求r=(msg,inactive)，在任務(wù)task執(zhí)行完成并發(fā)送消息msg后則產(chǎn)生需求r′=(msg,delivered)；規(guī)則R3和規(guī)則R4可按類似規(guī)則R1方式解釋；規(guī)則R2是指若存在需求r=(msg,delivered)，在任務(wù)task執(zhí)行完成，且未接收消息msg后則產(chǎn)生需求r′=(msg,pending)。

在明確需求產(chǎn)生規(guī)則之后，結(jié)合任務(wù)定義和格局可定義協(xié)同業(yè)務(wù)過程執(zhí)行語義。

(1)S為有窮格局集合。

(2)s0為初始格局。

(3){task,R}中R為任務(wù)task關(guān)聯(lián)原子需求集合，表示在task完成后所達(dá)到的需求。

1)·task?r[i]∧task.MsgRec?r.MS，表示若task可以執(zhí)行，則其使能且需要接收的消息均滿足；

2)s=r[M′/M]i∧s=r[MS′/MS]，表示若task執(zhí)行完成后，格局r中BPi的運(yùn)行狀態(tài)以及消息狀態(tài)分別更新為M′=(M-·task)∪task·和MS′=(MS-task.MsgRec)∪task.MsgSend；

3)?msg∈task.MsgRec∪task.MsgSend，若?μ∈Δ且μ.msg=msg，按需求產(chǎn)生式更新后為μ′，則μ′∈R且Δ=(Δ-μ)∪{μ′}。

由于協(xié)同業(yè)務(wù)過程執(zhí)行語義采用LTS描述，故可將其轉(zhuǎn)換為其他模型檢測工具可以識別的規(guī)約(如SMV、Promela等)進(jìn)行形式分析，從而判別出協(xié)同業(yè)務(wù)過程是否與期望需求一致。

3 基于模型檢測的需求一致性檢測

為了實(shí)現(xiàn)需求一致性自動檢測，本文采用模型驗(yàn)證技術(shù)，其基本思想是：將待驗(yàn)證的系統(tǒng)表示為一個狀態(tài)遷移模型M，需驗(yàn)證的性質(zhì)用時序邏輯公式φ表示，進(jìn)而就可以將“系統(tǒng)是否滿足所期望的性質(zhì)”轉(zhuǎn)化為“M是否滿足公式，即M|=φ”。目前，較為著名的模型驗(yàn)證工具有NuSMV、SPIN和FDR等?？紤]到NuSMV開源、具有開放式架構(gòu)和以SMV語言描述模型的行為可解釋為Kripke結(jié)構(gòu)(KS)等特點(diǎn)。故本文選用NuSMV作為需求一致性自動驗(yàn)證工具。

圖2所示為基于NuSMV的參與組織需求一致性自動檢測框架，具體檢測步驟如下：

步驟1將協(xié)同業(yè)務(wù)過程轉(zhuǎn)換為SM，之后將SM轉(zhuǎn)換為SMV規(guī)約。

步驟2采用DRDL描述參與組織需求，并將其轉(zhuǎn)換為LTL公式。

步驟3將SMV規(guī)約和LTL公式分別作為NuSMV的模型和性質(zhì)輸入，驗(yàn)證結(jié)果將表明協(xié)同業(yè)務(wù)過程是否滿足給定的參與組織需求。

如果驗(yàn)證結(jié)果得到了驗(yàn)證需求的反例，則說明協(xié)同業(yè)務(wù)過程與期望需求不一致，根據(jù)反例信息可以找到協(xié)同業(yè)務(wù)過程中存在的問題并進(jìn)行調(diào)整；如果驗(yàn)證結(jié)果沒有反例出現(xiàn)，則說明協(xié)同業(yè)務(wù)過程滿足期望性質(zhì)。特別地，由于使用模型檢測工具NuSMV，使得需求一致性驗(yàn)證過程可自動完成，不需要人工干預(yù)。

分析圖2所示的一致性驗(yàn)證框架可知，生成協(xié)同業(yè)務(wù)過程執(zhí)行語義和采用RDG描述參與組織需求在前文進(jìn)行詳細(xì)闡述。因此，為實(shí)現(xiàn)需求一致性自動檢測，需要重點(diǎn)解決將執(zhí)行語義模型轉(zhuǎn)換為NuSMV輸入語言和將RDG描述參與組織需求轉(zhuǎn)換為LTL公式這兩個問題。下面對這兩個問題進(jìn)行詳細(xì)討論。

3.1 執(zhí)行語義到Kripke結(jié)構(gòu)轉(zhuǎn)換

由于NuSMV的輸入語言是基于有限狀態(tài)自動機(jī)的形式語言，其行為解釋為Kripke結(jié)構(gòu)。將執(zhí)行語義模型轉(zhuǎn)換為NuSMV輸入語言的關(guān)鍵在于實(shí)現(xiàn)執(zhí)行語義模型到Kripke結(jié)構(gòu)的轉(zhuǎn)換。下面先給出Kripke結(jié)構(gòu)的定義。

定義11Kripke結(jié)構(gòu)[27]。設(shè)AP為非空原子命題集合，Kripke結(jié)構(gòu)形式化定義為4元組KS=(S,S0,R,L)，其中：

(1)S為有限狀態(tài)集合。

(2)S0?S為初始狀態(tài)集合。

(3)R?S×S為狀態(tài)遷移關(guān)系集合。

(4)L:S→2AP為標(biāo)記函數(shù)，用于實(shí)現(xiàn)狀態(tài)到AP冪集映射，表示返回在該狀態(tài)成立的原子命題集合。

(2)Sk0={s0}。

(4)對于?r，s∈S，L(r)={⊥}，L(s)={⊥}且L((r,a,s))={a}。

通過對LTS到KS轉(zhuǎn)換過程進(jìn)行分析，可得到轉(zhuǎn)換唯一性定理。

證畢。

定理1的結(jié)論確保了SM與KS間存在一對一映射關(guān)系。以此為基礎(chǔ)，并通過對轉(zhuǎn)換過程進(jìn)行歸納，得出定理2。

證明采用數(shù)學(xué)歸納法證明。

(2)當(dāng)n=k-1時，對SM第k-1次(記為SMk-1)轉(zhuǎn)換生成的Kripke結(jié)構(gòu)為KSk-1，滿足trace(SMk-1)≈trace(KSk-1)，其中函數(shù)trace(S)用來標(biāo)識S的跡。

證畢。

根據(jù)定理2，對于任意以RDG描述需求R具有如下重要結(jié)論。

定理3設(shè)SM為協(xié)同業(yè)務(wù)過程執(zhí)行語義模型，由其生成Kripke結(jié)構(gòu)為KS。需求R在SM和KS上具有相同滿足結(jié)果。

證明由定理2結(jié)論可知：SM和KS具有相同跡語義，則由文獻(xiàn)[28]結(jié)論可知，SM和KS滿足相同的時序邏輯規(guī)范，即對于任意LTL公式φ，公式φ在SM和KS具有相同驗(yàn)證結(jié)果。又因?yàn)樾枨驲在本文中采用線性時序邏輯公式LTL描述(參見3.2節(jié)),可推導(dǎo)出，需求R在SM和KS上具有相同滿足結(jié)果。

證畢。

基于定理3結(jié)論，對于任意以RDG描述參與組織需求R，有如下推論。

推論1設(shè)SM為協(xié)同業(yè)務(wù)過程生成語義模型，SL是根據(jù)定義9生成Kripke結(jié)構(gòu)對應(yīng)的SMV語言，需求R在SM滿足結(jié)果和SL上檢測結(jié)果一致。

證明基于KS，NuSMV輸入語言，即SMV語言中，狀態(tài)變量初始值用init()語句定義；對于?r∈R(R為KS中狀態(tài)遷移關(guān)系集合)，r在SMV語言中可由next-case語句進(jìn)行精確地刻畫。因此，由KS生成的SMV語言與KS間具有相同反應(yīng)式，即具有相同跡。而定理2結(jié)論又表明SM與KS之間是跡等價，從而可知：由KS生成的SMV語言與SM是跡等價的。結(jié)合定理3結(jié)論可推出：在R由LTL公式描述情況下，需求R在SM滿足結(jié)果和SL上檢測結(jié)果一致。

證畢。

在確保轉(zhuǎn)換正確前提下，根據(jù)定義10得到執(zhí)行語義模型到SMV語言轉(zhuǎn)換規(guī)則如表2所示。

表2 執(zhí)行語義模型SM到SMV語言轉(zhuǎn)換規(guī)則

續(xù)表2

3.2 需求到LTL公式轉(zhuǎn)換

將參與組織需求轉(zhuǎn)換成LTL公式分兩步進(jìn)行：①提出將參與組織需求中的需求依賴關(guān)系轉(zhuǎn)換為LTL公式規(guī)則集；②在上一步的基礎(chǔ)上，提出將參與組織需求轉(zhuǎn)換成LTL公式算法。

通過分析DRG中4種需求間的依賴關(guān)系，給出4條轉(zhuǎn)換規(guī)則用于將需求依賴關(guān)系統(tǒng)一轉(zhuǎn)換為LTL公式?！鬄長TL中存在算子，有關(guān)LTL的詳細(xì)內(nèi)容參見文獻(xiàn)[24]。

規(guī)則1若R=R1&…&Rn，則用LTL公式表示為◇R1∧…∧◇Rn。

規(guī)則2若R=R1‖…‖Rn，則用LTL公式表示為◇R1∨…∨◇Rn。

規(guī)則3若R=Ri?Rj，則用LTL公式表示為◇Ri→◇Rj。

規(guī)則4若Ri→Rj，則用LTL公式表示為◇(Ri∪Rj)。

設(shè)R為采用RDG描述參與組織需求，且具有良構(gòu)性。下面給出算法1來自動生成需求R對應(yīng)的LTL公式集合。算法1首先調(diào)用算法2生成相關(guān)節(jié)點(diǎn)對應(yīng)的LTL公式，然后按照規(guī)則3和規(guī)則4生成互斥關(guān)系和前驅(qū)關(guān)系對應(yīng)的LTL公式。

算法1 Generate LTL formula for R

Input:Requirement R=(V,E,φ);

Output:LTL formula set LS for R;

1. generate LTL formula rootLtl for root requirement root by algorithm 2 and add it to LS;

2. for each XOR R=Ri?Rjin R do

3. generate LTL formula liand ljfor Ri, Rj, respectively;

4. and add ◇li→◇ljto LS;

5. end for

6. for each precursor R=Ri→Rjin R do

7. generate LTL formula liand ljfor Ri, Rj, respectively;

9. end for

10. return LS;

算法2根據(jù)規(guī)則1和規(guī)則2生成需求R中任意節(jié)點(diǎn)v對應(yīng)的LTL公式，其時間復(fù)雜度為O(V)，其中V為需求R中節(jié)點(diǎn)數(shù)。

算法2 Generate LTL formula for given vertex v

Input:Requirement R=(V,E,φ);

Output:LTL formula for vertex v;

1. generate decomposition relation DR={v} and add DR to list list;

2. put v into queue Q;

3. while Q.size > 0 then

4. elem=Q.poll;

5. obtain decomposition type type by elem;

6. if type=AND then

7. get children children={c1,…,cn} of elem;

8. replace elem by children in DR where DR contains elem;

9. for each c in children do

10. if c is not leaf then

11. add c to Q;

12. end if

13. end for

14. else

15. obtain DR where DR contains elem;

16. construct set {c1}∪(DR-elem),…,{cn}∪(DR-elem);

17. delete DR in list;

18. and add each element in set to list;

19. end if

20. end while

21. ltl=null;

22. for each elem={e1,…,en} in list do

23. tempLtl=e1∧…∧en;

24. ltl=ltl∨tempLtl;

25. end for

26. return ltl;

根據(jù)3.1節(jié)和3.2節(jié)討論方法，可將協(xié)同業(yè)務(wù)過程和參與組織需求分別轉(zhuǎn)換為表達(dá)能力等價的SMV規(guī)約和以LTL公式表示的性質(zhì)。將轉(zhuǎn)換生成SMV規(guī)約和LTL公式分別作為NuSMV的模型和性質(zhì)輸入，NuSMV(其集成了基于LTL公式的模型檢測引擎)將自動完成需求一致性檢測。根據(jù)NuSMV檢測結(jié)果，可以判斷協(xié)同業(yè)務(wù)過程是否與需求一致。若存在不一致，則根據(jù)反例信息可以找到協(xié)同業(yè)務(wù)過程中存在的問題并予以修正。

4 實(shí)例分析

4.1 實(shí)例說明

為說明本文所提方法在建模和分析時的有效性，本節(jié)以協(xié)同制造中一個簡化的采購訂單(記為PO)為例對其進(jìn)行建模，并與屬于該方法內(nèi)的典型文獻(xiàn)[11]進(jìn)行對比分析。該采購訂單中包含1個零售商、1個制造商和1個產(chǎn)品送貨商，其交互過程如圖3所示。首先，零售商與制造商就訂購產(chǎn)品價格進(jìn)行反復(fù)協(xié)商(步驟1)，在價格達(dá)成一致后零售商向制造商提交訂單(步驟2)；其次，制造商在收到該訂購請求后向送貨商發(fā)送運(yùn)輸請求(步驟3)，送貨商在收到運(yùn)輸請求后確定運(yùn)輸費(fèi)用并通知制造商(步驟4)。在收到運(yùn)費(fèi)請求后制造商先向零售商請求支付訂購產(chǎn)品(步驟5)，接著在零售商支付完成后(步驟6)向送貨商付費(fèi)(步驟7)；最后，送貨商在收到制造商付費(fèi)消息后將訂購產(chǎn)品送至零售商(步驟8)。

4.2 采購訂單建模

采購訂單PO建?？砂慈缦聝刹竭M(jìn)行：

(1)建模采購訂單PO對應(yīng)協(xié)同業(yè)務(wù)過程

通過分析圖3中PO的交互過程，采用Petri網(wǎng)建模零售商、制造商和送貨商各自的業(yè)務(wù)過程控制流分別如圖4a～圖4c所示，其中每個變遷標(biāo)識(如r1等)為其對應(yīng)任務(wù)標(biāo)識。

進(jìn)一步分析，可得到PO中每個參與組織控制流中涉及任務(wù)信息如表3所示。

表3 采購訂單中任務(wù)信息

續(xù)表3

將零售商、制造商和送貨商對應(yīng)的業(yè)務(wù)過程根據(jù)定義6并發(fā)組合得到采購訂單的協(xié)同業(yè)務(wù)過程。根據(jù)定義10生成PO執(zhí)行語義如圖5a所示，繼而根據(jù)定義12將其轉(zhuǎn)換為KS如圖5b所示。

圖5中，每個任務(wù)完成后所達(dá)到的需求如表4所示。

表4 任務(wù)需求關(guān)聯(lián)表

(2)建模參與組織需求

參與組織需求可由參與組織間協(xié)商得到，其隱含意圖是能夠?qū)崿F(xiàn)參與組織間的價值交換[26]，例如零售商支付，而制造商提供產(chǎn)品就是一類典型價值交換過程?；谠撛瓌t，PO中參與組織需求R采用RDG描述如圖6a所示，其中需求Order表示若制造商提供訂購產(chǎn)品(rr7)，則零售商支付(rr6)，且零售商在制造商提供訂購產(chǎn)品之前完成支付(rr6→rr7)；需求ShipGoods表示若送貨商運(yùn)送訂購產(chǎn)品至零售商(rr7)，則制造商支付運(yùn)費(fèi)(rm9)，且制造商在送貨商運(yùn)送訂購產(chǎn)品之前完成支付(rm9→rr7)。需要說明是，圖6a僅僅描述參與組織間存在一類共性需求，需求R可根據(jù)實(shí)際情況做進(jìn)一步細(xì)化。

根據(jù)算法1將圖6a所示需求R轉(zhuǎn)換為LTL公式，如性質(zhì)1～性質(zhì)3所示。

性質(zhì)1(◇payOrder=delivered∧◇orderGoods=received∧◇payshipGoodes=delivered)。

性質(zhì)2(◇(payOrder=delivered∪orderGoods=received))。

性質(zhì)3(◇(payshipGoodes=delivered∪orderGoods=received))。

4.3 方法評價

為評價本文方法的有效性，選擇此類方法中具有代表性的工作[10]。文獻(xiàn)[10]提出的需求一致性驗(yàn)證方法針對單個業(yè)務(wù)過程，不能直接應(yīng)用于跨組織環(huán)境下需求一致性驗(yàn)證。但在求得協(xié)同業(yè)務(wù)過程執(zhí)行語義和明確參與組織需求前提下，文獻(xiàn)[10]方法也可用于協(xié)同業(yè)務(wù)過程需求一致性驗(yàn)證。因此，以PO為對象，對本文方法和文獻(xiàn)[10]方法的有效性進(jìn)行定性評價。

有效性是指針對任意結(jié)構(gòu)的協(xié)同業(yè)務(wù)過程，本文方法和文獻(xiàn)[10]方法能否識別出PO滿足既定需求。由于協(xié)同業(yè)務(wù)過程的執(zhí)行語義以LTS刻畫，本質(zhì)上，LTS是一個有向圖，故對于任意LTS而言，遷移集間只存在順序和循環(huán)兩種關(guān)系。因此，針對PO首先構(gòu)建有環(huán)結(jié)構(gòu)協(xié)同業(yè)務(wù)過程，記為LCBP，即PO中存在零售商和制造商間就訂購產(chǎn)品價格進(jìn)行反復(fù)協(xié)商交互；然后構(gòu)建無環(huán)結(jié)構(gòu)協(xié)同業(yè)務(wù)過程，記為NLCBP，即將PO中零售商和制造商間就訂購產(chǎn)品價格進(jìn)行反復(fù)協(xié)商交互移除。同時，為了評價能否識別既定需求，先以圖6a所示需求R作為目標(biāo)需求進(jìn)行評價。由于PO滿足需求R，故記此時需求為CR；然后同時將圖6a中需求shipGoods注入一個外部需求re=(r,delivered)，得到需求記為ER，如圖6b所示，和如圖5b KS中節(jié)點(diǎn)P1617關(guān)聯(lián)外部需求re=(r,delivered)，表示PO在執(zhí)行至P1617時，同時滿足需求(payshipGoodes,delivered)和re=(r,delivered)，即rm9={(payshipGoodes,delivered),(r,delivered)}，記此時采購訂單對應(yīng)協(xié)同業(yè)務(wù)過程為ELCBP，且無環(huán)情形下采購訂單對應(yīng)協(xié)同業(yè)務(wù)過程記為ENLCBP。

使用本文方法和文獻(xiàn)[10]方法在LCBP、NLCBP檢測需求CR和在ELCBP、ENLCBP上檢測需求ER，檢測結(jié)果分別如表5和表6所示。表5和表6中，√表示檢測結(jié)果為True，×表示檢測結(jié)果為False，?表示不支持檢測。

表5 兩種方法CR檢測結(jié)果

由表5可以看出：針對LCBP，文獻(xiàn)[10]方法檢測結(jié)果為?。其原因在于：文獻(xiàn)[10]方法采用任務(wù)系列匹配方式，即在檢測之前需要求取所有的任務(wù)執(zhí)行系列，由于LCBP中存在環(huán)結(jié)構(gòu)，這將導(dǎo)致需求一致性無法判定。而本文方法檢測結(jié)果為√，表示能夠成功檢測出LCBP滿足需求CR。其原因在于：本文方法采用模型檢測技術(shù)，該技術(shù)可有效處理過程模型中含有環(huán)結(jié)構(gòu)情形。其思想是將以LTL公式描述的需求轉(zhuǎn)換為Büchi自動機(jī)，過程模型以有限狀態(tài)機(jī)刻畫，通過判定Büchi自動機(jī)與有限狀態(tài)機(jī)的積(也為自動機(jī))中是否存在強(qiáng)連通組件來判斷需求是否滿足[28]。針對NLCBP，本文方法和文獻(xiàn)[10]方法均能夠成功檢測出NLCBP滿足需求CR。

表6 兩種方法ECR檢測結(jié)果

由表6可以看出：針對ELCBP，文獻(xiàn)[10]方法檢測結(jié)果為?，其原因在表5分析中進(jìn)行闡述。而本文方法檢測結(jié)果為√，表示能夠成功檢測出LCBP滿足需求CR。針對NLCBP，文獻(xiàn)[10]方法檢測結(jié)果為×，而本文方法檢測結(jié)果為√。其原因在于：文獻(xiàn)[10]方法采用任務(wù)系列匹配方式實(shí)現(xiàn)需求一致性檢測，需求以任務(wù)計劃[29]形式描述，故僅能檢測出需求(payshipGoodes,delivered)，(r,delivered)存在次序關(guān)系情形，無法檢測出上述需求同時發(fā)生情形。而本文方法采用LTL公式(◇payOrder=delivered∧◇orderGoods=received∧◇payshipGoodes=delivered∧◇r=delivered)描述需求ER，可方便地表述出需求(payshipGoodes,delivered)和(r,delivered)間次序滿足和同時滿足情形，因此檢測結(jié)果為√。

綜上所述，在需求描述方面，由于本文方法采用LTL公式表示需求，較文獻(xiàn)[10]方法中任務(wù)計劃描述能力更強(qiáng)，即所有用任務(wù)計劃描述需求均轉(zhuǎn)換成LTL公式[29]。此外，跨組織環(huán)境下需求間通常存在次序滿足和同時滿足情形，采用LTL公式均可直觀描述。在需求一致性檢測方面，文獻(xiàn)[10]方法無法處理過程模型中存在環(huán)結(jié)構(gòu)情形，而本文方法能夠有效應(yīng)對此類情況，適用性更強(qiáng)。因此可得出如下結(jié)論：相較文獻(xiàn)[10]方法，本文方法一方面可直接應(yīng)用于建?？缃M織需求和支持需求分析過程模型；另一方面可更加有效地刻畫參與組織需求和進(jìn)行需求一致性驗(yàn)證。

5 結(jié)束語

參與組織需求是協(xié)同業(yè)務(wù)過程形式驗(yàn)證中需要考慮的一個重要方面。本文基于模型檢測技術(shù)提出一種驗(yàn)證參與組織共性及個性需求方法。該方法一方面將協(xié)同業(yè)務(wù)過程轉(zhuǎn)換成語義等價SMV語言，從理論上確保驗(yàn)證結(jié)果一致性；另一方面，提出將由RDG描述的參與組織需求轉(zhuǎn)換成LTL公式算法。進(jìn)而借助符號模型檢測工具NuSMV實(shí)現(xiàn)在協(xié)同業(yè)務(wù)過程上自動檢測參與組織需求滿足問題。由于協(xié)同業(yè)務(wù)過程規(guī)模通常較為復(fù)雜，使用模型檢測技術(shù)驗(yàn)證參與組織需求一致性可能面臨的狀態(tài)空間爆炸問題。為此，未來將從以下3個方面開展研究：①在考慮確保檢測結(jié)果一致前提下，如何采用抽象、分解等方法來提高需求一致性形式驗(yàn)證效率；②本文將RDG中約束關(guān)系(即Pre關(guān)系和XOR關(guān)系)限定在同一分解層次，在實(shí)際應(yīng)用中，約束關(guān)系也可能分布在不同層次，未來工作將放松這一限制，使得本文提出的方法更具普適性；③在跨組織環(huán)境下，不同參與組織的需求可能有天然的不一致性，如何消除這種不一致將在未來工作中進(jìn)行詳細(xì)討論。