以數(shù)據(jù)為中心的業(yè)務(wù)流程系統(tǒng)建模與驗(yàn)證問(wèn)題研究.pdf

1、I學(xué)校代碼：10255學(xué)號(hào)：2121521碩士研究生學(xué)位論文碩士研究生學(xué)位論文以數(shù)據(jù)數(shù)據(jù)為中心的業(yè)務(wù)流程系統(tǒng)建模為中心的業(yè)務(wù)流程系統(tǒng)建模與驗(yàn)證問(wèn)題研究驗(yàn)證問(wèn)題研究學(xué)科專(zhuān)業(yè)：學(xué)科專(zhuān)業(yè)：軟件工程軟件工程姓名：萬(wàn)小妹萬(wàn)小妹指導(dǎo)教師：指導(dǎo)教師：劉國(guó)華劉國(guó)華答辯日期：答辯日期：2015年1月III以數(shù)據(jù)為中心的業(yè)務(wù)流程系統(tǒng)建模及驗(yàn)證問(wèn)題研究摘要以數(shù)據(jù)為中心是業(yè)務(wù)流程管理技術(shù)發(fā)展的一個(gè)新趨勢(shì)。artifact是業(yè)務(wù)流程中的關(guān)鍵數(shù)據(jù)實(shí)體以artifa

2、ct為中心的業(yè)務(wù)流程管理是以數(shù)據(jù)為中心的業(yè)務(wù)流程管理的典型代表。業(yè)務(wù)流程系統(tǒng)模型是業(yè)務(wù)流程管理的基礎(chǔ)它必須滿(mǎn)足一些政府政策、法律法規(guī)以及商業(yè)規(guī)則等約束條件。本文把描述邏輯引入到系統(tǒng)建模中，提出了一個(gè)以artifact為中心的業(yè)務(wù)流程系統(tǒng)模型，并給出了兩個(gè)不同系統(tǒng)之間的互為相似性的充分條件。業(yè)務(wù)流程系統(tǒng)必須滿(mǎn)足法律法規(guī)、政府政策及商業(yè)規(guī)則等約束條件。對(duì)于以artifact為中心的業(yè)務(wù)流程系統(tǒng)，本文首先采用FOCTL(Firstderext

3、ensionofcomputationlogic)表達(dá)這些約束條件。然后，證明判定系統(tǒng)是否滿(mǎn)足約束是不可判定問(wèn)題。尋找與其互為相似的具有有限狀態(tài)且可計(jì)算的剪枝系統(tǒng)。證明如果與其互為相似的系統(tǒng)滿(mǎn)足約束，那么原系統(tǒng)也滿(mǎn)足。最后，采用已發(fā)展成熟的標(biāo)準(zhǔn)模型檢測(cè)算法判斷具有限狀態(tài)且可計(jì)算的剪枝系統(tǒng)是否滿(mǎn)足約束，從而達(dá)到驗(yàn)證原系統(tǒng)的目的。artifact由信息模型和生命周期兩部分組成。信息模型描述artifact的數(shù)據(jù)結(jié)構(gòu)。生命周期描述artifa

4、ct從創(chuàng)建、修改到完成并歸檔的處理軌跡，它是由業(yè)務(wù)部門(mén)根據(jù)業(yè)務(wù)規(guī)則和其他有關(guān)業(yè)務(wù)的約束條件來(lái)定義，主要用于業(yè)務(wù)的合規(guī)性檢查和流程實(shí)時(shí)監(jiān)控。因此，生命周期的驗(yàn)證和aritfact有效性驗(yàn)證是以artifact為中心的業(yè)務(wù)流程系統(tǒng)中關(guān)鍵的驗(yàn)證問(wèn)題。針對(duì)這兩類(lèi)問(wèn)題，本文通過(guò)枚舉不同類(lèi)型的生命周期實(shí)例，判斷生命周期的正確性，通過(guò)利用artifact生命周期研究artifact的有效性問(wèn)題。以artifact為中心的業(yè)務(wù)流程是以數(shù)據(jù)為中心的典型代