[發(fā)明專利]BPMN的形式化分析和驗證方法

無效

• 申請?zhí)枺?/td>: 200910068656.6
• 申請日: 2009-04-28
• 公開（公告）號: CN101877079A
• 公開（公告）日: 2010-11-03
• 發(fā)明（設(shè)計）人: 朱明英
• 申請（專利權(quán)）人: 朱明英
• 主分類號: G06Q10/00
• 分類號: G06Q10/00
• 代理公司: 暫無信息
• 代理人: 暫無信息

1.BPMN的形式化分析和驗證方法，其特征在于包括下列幾點：

一個BPMN模型是一個四元組P＝(O，F(xiàn)，fCond，fExcp)；

采用COWS對BPMN核心元素建模；

采用COWS公式描述BPMN結(jié)構(gòu)正確性；

采用COWS推演對BPMN相容性進(jìn)行分析。

2.如權(quán)利要求1所述的方法，其特征在于，對BPMN模型進(jìn)行抽象語法描述。一個BPMN模型是一個四元組：P＝(O，F(xiàn)，fCond，fExcp)，其中，O是對象集，分為不相交的活動集A，事件集E和網(wǎng)關(guān)集G；表示控制流關(guān)系，是連接對象的順序流集；fCond是將網(wǎng)關(guān)出來的順序流映射為條件的函數(shù)，F(xiàn)⌒(G×O)→C，其中，C代表所有可能條件；fExcp建立中間事件和某活動的連接關(guān)系，表明該事件發(fā)生觸發(fā)異常，中斷該活動的執(zhí)行。

3.如權(quán)利要求1所述的方法，其特征在于，采用COWS對元素模型建立語義。BPMN模型描述的業(yè)務(wù)流程對應(yīng)COWS中多個服務(wù)的組合服務(wù)。邏輯上單獨的原子任務(wù)作為一個COWS服務(wù)，當(dāng)需要對某個復(fù)雜的單一活動進(jìn)行內(nèi)部邏輯驗證和流程分析時，也可將其分割為幾個具有一定邏輯關(guān)系的COWS服務(wù)。BPMN中通過消息流在不同池之間傳遞的消息，對應(yīng)于COWS中服務(wù)間通信的參數(shù)，即變量或名稱。BPMN中活動之間消息的傳遞過程，對應(yīng)于COWS中服務(wù)之間的通信。BPMN中的池和道，代表流程中的參與者，對應(yīng)于組成COWS中的伙伴；池內(nèi)部的操作對應(yīng)COWS對端點的操作。BPMN中的空任務(wù)，對應(yīng)于COWS中的空服務(wù)0。BPMN的異常，對應(yīng)COWS中的異常。

4.如權(quán)利要求1所述的方法，其特征在于，對模型結(jié)構(gòu)的正確性進(jìn)行形式化描述。模型中不存在永遠(yuǎn)也不可能執(zhí)行到的活動。如果用COWS標(biāo)簽變遷，則從開始事件對應(yīng)的服務(wù)es，存在變遷序列α0，α1，…，αn，演變?yōu)槟郴顒訉?yīng)的服務(wù)a，表示為流程的任何一個活動執(zhí)行序列，都可以到達(dá)結(jié)束事件ee。

5.如權(quán)利1要求所描述的方法，其特征在于，根據(jù)COWS推演得到系統(tǒng)協(xié)作正確性。給定一個完整BPMN流程的COWS形式化模型，如果該模型能最終演化為0服務(wù)，則該流程是協(xié)作正確的，也即服務(wù)間是相容的。判定給定的系統(tǒng)是否相容，只需判定系統(tǒng)COWS模型的并發(fā)執(zhí)行能否最終演變成空服務(wù)。而驗證系統(tǒng)協(xié)作的正確性問題，就可以轉(zhuǎn)化成對COWS模型進(jìn)行推演，看是否最終能演化為空服務(wù)。