工作流模型正確性驗(yàn)證問(wèn)題研究.pdf

1、本文首先綜述了當(dāng)前工作流模型及其驗(yàn)證方法,著重介紹了基于Petri網(wǎng)進(jìn)行工作流建模和驗(yàn)證的優(yōu)缺點(diǎn),然后提出了一個(gè)基于雙分支條件有向圖(Double-Road Conditional Directed Graph(DCDG))的工作流模型,該模型是一個(gè)工作流實(shí)際業(yè)務(wù)流程的抽象,它建立在狀態(tài)圖和ECA規(guī)則的基礎(chǔ)上,具有較強(qiáng)的表達(dá)力和直觀的圖形描述,同時(shí)底層通訊機(jī)制基于對(duì)象和ECA規(guī)則,便于進(jìn)行語(yǔ)義化描述.工作流模型正確性驗(yàn)證問(wèn)題是工作流研究

2、領(lǐng)域中的一個(gè)重要問(wèn)題,工作流管理系統(tǒng)可能建立錯(cuò)誤的工作流模型,導(dǎo)致工作流的執(zhí)行出現(xiàn)異常.有的研究者將事件平衡分析方法引入了工作流模型,通過(guò)分析局部工作流的控制邏輯,提出了驗(yàn)證工作流控制邏輯正確性的一個(gè)必要條件,但是并沒有涉及到如何解決整個(gè)工作流的控制邏輯正確性驗(yàn)證問(wèn)題.本文在基于雙分支條件有向圖的工作流模型基礎(chǔ)上,提出了一種驗(yàn)證整個(gè)工作流控制邏輯正確性的方法,實(shí)驗(yàn)結(jié)果表明,該方法是可行的.工作流管理系統(tǒng)中的時(shí)間管理問(wèn)題是工作流研究領(lǐng)域中

3、另一個(gè)重要的問(wèn)題,通過(guò)對(duì)工作流活動(dòng)加以時(shí)間約束,可以保證工作流正確、高效的執(zhí)行.目前,許多研究者對(duì)工作流模型中時(shí)間屬性進(jìn)行建模,進(jìn)行了一些有益的工作,但是對(duì)于工作流活動(dòng)時(shí)間約束的正確性驗(yàn)證問(wèn)題和時(shí)序邏輯的推理問(wèn)題沒有深入的討論.本文首先分析了工作流管理系統(tǒng)中主要應(yīng)該考慮的時(shí)間問(wèn)題,然后在雙分支條件有向圖模型基礎(chǔ)上進(jìn)行了一些關(guān)于時(shí)序邏輯推理問(wèn)題的研究,提出了四個(gè)推理規(guī)則,同時(shí)提出了驗(yàn)證工作流活動(dòng)時(shí)間約束正確性的一些必要條件.另外,本文提出