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

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

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

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