基于時間模式分析的業(yè)務(wù)流程模型驗證方法.pdf

1、隨著業(yè)務(wù)流程模型的廣泛應(yīng)用，其正確性顯得尤為重要。時間約束決定了業(yè)務(wù)流程能否正確執(zhí)行，任何一點時間延遲都有可能造成極大的資源浪費，所以對時間約束進(jìn)行驗證是檢測業(yè)務(wù)流程模型正確性非常重要的環(huán)節(jié)。本文以時間模式分析為基礎(chǔ)，研究了基于時間模式分析的業(yè)務(wù)流程模型驗證方法，具體工作如下：
　　首先，提出了基于形式化語義的時間模式分析方法。根據(jù)業(yè)務(wù)流程模型中常見的時間約束類型將時間模式分為持續(xù)時間模式、固定時刻模式與周期循環(huán)模式三類，給出了業(yè)

2、務(wù)流圖、時間區(qū)間以及三類時間模式的形式化描述。定義了時間模式的可滿足性，提出了周期循環(huán)模式到持續(xù)時間模式的轉(zhuǎn)換規(guī)則，證明了可滿足性保持定理，即業(yè)務(wù)流圖滿足周期循環(huán)模式當(dāng)且僅當(dāng)滿足轉(zhuǎn)換后的持續(xù)時間模式。
　　其次，提出了基于時間模式分析的業(yè)務(wù)流程模型驗證方法。針對業(yè)務(wù)流程模型的結(jié)構(gòu)、行為、流程等一致性問題提出了驗證框架，基于時間模式分析設(shè)計了業(yè)務(wù)流程模型靜態(tài)結(jié)構(gòu)、動態(tài)行為和業(yè)務(wù)流圖到Prolog的轉(zhuǎn)換規(guī)則與轉(zhuǎn)換算法，以及靜態(tài)結(jié)構(gòu)一致

3、性、動態(tài)行為一致和時間模式一致性到Prolog的轉(zhuǎn)換規(guī)則。以醫(yī)療流程模型為例進(jìn)行了模型一致性驗證和修復(fù)。與相關(guān)工作對比表明本文的方法可以全面地驗證業(yè)務(wù)流模型一致性。
　　最后，基于業(yè)務(wù)流程模型時間模式分析與一致性驗證方法設(shè)計實現(xiàn)了業(yè)務(wù)流程模型驗證平臺。該平臺以GMF為基礎(chǔ)，設(shè)計了業(yè)務(wù)流程模型建模模塊、靜態(tài)結(jié)構(gòu)與動態(tài)行為驗證模塊以及業(yè)務(wù)流圖驗證模塊，實現(xiàn)了從業(yè)務(wù)流程模型建模到模型的靜態(tài)結(jié)構(gòu)一致性、動態(tài)行為一致性以及時間模式一致性的自