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

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

0 引言

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

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

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

本文主要貢獻如下：

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

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

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

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

1 相關研究

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

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

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

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

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

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

2.1 需求依賴圖RDG

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

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

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

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

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

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

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

進一步以G為基礎，參與組織需求良構性定義如下。

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

(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)結構。

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

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

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

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

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

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

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

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

(1)msg為消息。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(2)s0為初始格局。

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

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

2)s=r[M′/M]i∧s=r[MS′/MS]，表示若task執(zhí)行完成后，格局r中BPi的運行狀態(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è)務過程執(zhí)行語義采用LTS描述，故可將其轉換為其他模型檢測工具可以識別的規(guī)約(如SMV、Promela等)進行形式分析，從而判別出協(xié)同業(yè)務過程是否與期望需求一致。

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

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

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

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

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

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

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

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

3.1 執(zhí)行語義到Kripke結構轉換

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

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

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

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

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

(4)L:S→2AP為標記函數(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轉換過程進行分析，可得到轉換唯一性定理。

證畢。

定理1的結論確保了SM與KS間存在一對一映射關系。以此為基礎，并通過對轉換過程進行歸納，得出定理2。

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

(2)當n=k-1時，對SM第k-1次(記為SMk-1)轉換生成的Kripke結構為KSk-1，滿足trace(SMk-1)≈trace(KSk-1)，其中函數(shù)trace(S)用來標識S的跡。

證畢。

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

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

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

證畢。

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

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

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

證畢。

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

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

續(xù)表2

3.2 需求到LTL公式轉換

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

通過分析DRG中4種需求間的依賴關系，給出4條轉換規(guī)則用于將需求依賴關系統(tǒng)一轉換為LTL公式?！鬄長TL中存在算子，有關LTL的詳細內(nèi)容參見文獻[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)。

設R為采用RDG描述參與組織需求，且具有良構性。下面給出算法1來自動生成需求R對應的LTL公式集合。算法1首先調(diào)用算法2生成相關節(jié)點對應的LTL公式，然后按照規(guī)則3和規(guī)則4生成互斥關系和前驅關系對應的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é)點v對應的LTL公式，其時間復雜度為O(V)，其中V為需求R中節(jié)點數(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è)務過程和參與組織需求分別轉換為表達能力等價的SMV規(guī)約和以LTL公式表示的性質(zhì)。將轉換生成SMV規(guī)約和LTL公式分別作為NuSMV的模型和性質(zhì)輸入，NuSMV(其集成了基于LTL公式的模型檢測引擎)將自動完成需求一致性檢測。根據(jù)NuSMV檢測結果，可以判斷協(xié)同業(yè)務過程是否與需求一致。若存在不一致，則根據(jù)反例信息可以找到協(xié)同業(yè)務過程中存在的問題并予以修正。

4 實例分析

4.1 實例說明

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

4.2 采購訂單建模

采購訂單PO建?？砂慈缦聝刹竭M行：

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

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

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

表3 采購訂單中任務信息

續(xù)表3

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

圖5中，每個任務完成后所達到的需求如表4所示。

表4 任務需求關聯(lián)表

(2)建模參與組織需求

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

根據(jù)算法1將圖6a所示需求R轉換為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]。文獻[10]提出的需求一致性驗證方法針對單個業(yè)務過程，不能直接應用于跨組織環(huán)境下需求一致性驗證。但在求得協(xié)同業(yè)務過程執(zhí)行語義和明確參與組織需求前提下，文獻[10]方法也可用于協(xié)同業(yè)務過程需求一致性驗證。因此，以PO為對象，對本文方法和文獻[10]方法的有效性進行定性評價。

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

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

表5 兩種方法CR檢測結果

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

表6 兩種方法ECR檢測結果

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

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

5 結束語

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