基于狀態(tài)空間的工作流模型驗(yàn)證

1、基于狀態(tài)空間的工作流模型驗(yàn)證 基于狀態(tài)空間的工作流模型驗(yàn)證趙 磊 錢樂秋 趙文耘(復(fù)旦大學(xué)計(jì)算機(jī)與信息技術(shù)系,上海 )!#9:;5:35?a%1b1c!d$23摘 要 工作流模型的正確性和可靠性是工作流管理系統(tǒng)健壯性的基礎(chǔ)。該文提出一種基于狀態(tài)空間的工作流模型驗(yàn)證方法,從而確保在構(gòu)造期間產(chǎn)生有效的工作流模型。關(guān)鍵詞 工作流模式 依賴 斷言 狀態(tài)空間 驗(yàn)證算法文章編號 %!:&%:(!#)%:!: 文獻(xiàn)標(biāo)識碼 e 中圖分類號 f+%!#$%&#$ #&$* +$,-.-#-/0 /. 1/,2.3/4 5/*$367#/ 8$- 9-#0 8$:-; 67#/ 1$0;0(,2g3$ h7 h;

2、ga324 i j7h4; f2klhh?,mai 65n$,8l?l5 !#)&,#:fl2 kh442k32oo i 425p553 h7 qh4r7hq ;hi2 5o 3l2 p2oo h7 3l2 qh4r7hq ;?2;23oo32;$fl5o 435k2 5i5k32o o332:ogk2 po2i n24575k ;23lhi h7 qh4r7hq ;hi2,3h 2oa42 g4hiak5? 3l2 2772k35n2qh4r7hq ;hi2 5 3l2 pa5i5? 35;2$?$4/,*&:qh4r7hq okl2;2,i2g2i2k,g42i5k32,o332:ogk2

3、,n24575k ?h453l;將工作流模型的正確性歸納為工作流網(wǎng)的完整性,并提出了一% 引言種基于 網(wǎng)的圖形化簡方法輔助模型驗(yàn)證,但是其提出的+2345作為實(shí)現(xiàn)企業(yè)經(jīng)營過程自動化的一種有效手段,工作流技化簡步驟由于不具備完備性并不能完全驗(yàn)證工作流模型的正術(shù)自 !世紀(jì) &年代產(chǎn)生以來,在各方面都已經(jīng)有了長足的進(jìn)確性;而且 +2345網(wǎng)對于大多數(shù)用戶來說顯得過于復(fù)雜,不容易步和發(fā)展。在各種工作流相關(guān)技術(shù)中,工作流的有效建模是開掌握。發(fā)健壯的、合理的大型工作流系統(tǒng)的關(guān)鍵。綜合上面的方法,現(xiàn)有工作流建模技術(shù),無論是以 6.-活組織提出的 語言是描述工作流模型的良好方 *+,-動圖描述,抑或是以 網(wǎng)描

4、述,通常是將工作流建模為活動+2345法。但是由于 *.-語言沒有堅(jiān)實(shí)的數(shù)學(xué)基礎(chǔ)和邏輯基礎(chǔ),使得的遷移。這種方式是比較直觀的,但在進(jìn)行工作流驗(yàn)證的時(shí)候,由其描述的模型的一致性無法得到保證。會由于缺少行之有效的形式化表示而難以進(jìn)行?，F(xiàn)有的工作流建模通常關(guān)注于工作流的圖形化表示,而很該文提出的基于狀態(tài)空間搜索的工作流驗(yàn)證方法,將工作少關(guān)心工作流模型的計(jì)算機(jī)驗(yàn)證的可能性。對于小型的、簡單流建模為一種類似于狀態(tài)圖的形式。其基本思想是將工作流看的工作流系統(tǒng),開發(fā)人員可以比較容易地分析工作流活動之間作狀態(tài)空間中的序列,這樣,產(chǎn)生有效的工作流模式的問題就的邏輯相關(guān)性,從而確保工作流模型的有效性;但是對于大型

5、轉(zhuǎn)化為根據(jù)條件和約束搜索狀態(tài)空間的問題。該文后面會給出的、包含數(shù)十個(gè)甚至數(shù)百個(gè)活動的工作流系統(tǒng),單憑依靠開發(fā)將工作流模式由傳統(tǒng)的活動序列轉(zhuǎn)化為狀態(tài)序列,并對其加以人員的人力判斷,無法保證工作流是否完備、是否無二義性、是形式化表示,使其支持機(jī)器自動驗(yàn)證的全過程。否無死鎖等等。該文提出一種基于狀態(tài)空間的工作流模型的形式化驗(yàn)證工作流模式方法。這樣,在工作流的構(gòu)造階段,就可以對工作流模型進(jìn)行自 動化驗(yàn)證。工作流模式定義$%工作流管理系統(tǒng)(7.8)從辦公自動化工具演化而來。一! 工作流驗(yàn)證方法現(xiàn)狀 個(gè)工作流過程定義(或者工作流模式)是業(yè)務(wù)過程的一個(gè)形式由于工作流模型的復(fù)雜性,目前還沒有有效的算法可以對

6、化模型。它通常由聯(lián)合起來實(shí)現(xiàn)某一業(yè)務(wù)目標(biāo)的復(fù)合任務(wù)和原工作流模型的正確性進(jìn)行分析。文獻(xiàn)/%0提出一種基于圖形化簡 始活動組合而成。這些任務(wù)通常被組織成有向圖,弧表示活動的方法進(jìn)行工作流模型驗(yàn)證,并歸納了幾種化簡規(guī)則,但這種 之間的控制流。工作流被建模成過程圖 !(,#),是任務(wù)集方法只對工作流模型結(jié)構(gòu)中存在的特殊問題進(jìn)行了分析與驗(yàn) 合,#是轉(zhuǎn)換條件的集合。任務(wù)被分配給代理 (人或軟件或兩證,而且這種方法不適用于存在循環(huán)結(jié)構(gòu)的工作流模型。 者)用于順序或并發(fā)執(zhí)行。一個(gè)工作流模式被初始化多次,多個(gè)文獻(xiàn)/10中提出了用 +2345網(wǎng)進(jìn)行工作流建模的工作流網(wǎng), 實(shí)例可以在工作流執(zhí)行引擎中同時(shí)運(yùn)行。一個(gè)

7、工作流模式必須基金項(xiàng)目:國家 &d高技術(shù)研究發(fā)展計(jì)劃項(xiàng)目基金資助作者簡介:趙磊,男,復(fù)旦大學(xué)計(jì)算機(jī)系碩士研究生。研究方向:軟件工程,工作流技術(shù)。錢樂秋,男,復(fù)旦大學(xué)計(jì)算機(jī)系教授,博士生導(dǎo)師。研究方向:面向?qū)ο蠹夹g(shù),軟件復(fù)用技術(shù),軟件過程工程。趙文耘,男,復(fù)旦大學(xué)計(jì)算機(jī)系教授,博士生導(dǎo)師。研究方向:軟件工程,構(gòu)件技術(shù),軟件重用技術(shù)。! !#$% 計(jì)算機(jī)工程與應(yīng)用有足夠的表達(dá)能力來表達(dá)業(yè)務(wù)過程的結(jié)構(gòu)。一個(gè)任務(wù)可以是原子的,也可以是復(fù)合的。復(fù)合任務(wù)促進(jìn)了工作流模式定義的重用。圖 展示了復(fù)旦大學(xué)辦公自動化系統(tǒng)中,一個(gè)簡化的公文%流轉(zhuǎn)工作流模式實(shí)例。圖 !圖 %圖 !( .)描述了對圖 !( )虛線框中

8、部分的狀態(tài)重構(gòu):當(dāng) !任務(wù)的 #%輸入斷言集滿足時(shí),執(zhí)行 !任務(wù),執(zhí)行完畢轉(zhuǎn)入 %/&$! 依賴與斷言狀態(tài);同樣的,當(dāng) 任務(wù)的 輸入斷言集滿足時(shí),執(zhí)行 任一個(gè)工作流應(yīng)用可以表示為一系列任務(wù)( )以及它們 !& #% !&*務(wù);這里 !&任務(wù)根據(jù)執(zhí)行的結(jié)果可能轉(zhuǎn)入 !/狀態(tài)。其后,由之間的依賴關(guān)系。一個(gè)任務(wù)是一個(gè)特定的活動。依賴指相連任, 狀態(tài)到 狀態(tài)進(jìn)行一次遷移為合并的轉(zhuǎn)化,這種合并務(wù)之間的關(guān)系。不同任務(wù)之間可能有兩種依賴關(guān)系: %/ !/ &可以被看作一種偽活動。這樣,就完成了一次活動到狀態(tài)的重( %)通知依賴構(gòu)。更復(fù)雜的重構(gòu)方式將在今后的研究過程中詳細(xì)考察。通知依賴指前一任務(wù)完成后,發(fā)送一

9、個(gè)通知給后一任務(wù),從而激發(fā)后一任務(wù)。( !)數(shù)據(jù)流依賴 # 基于狀態(tài)空間的工作流表示數(shù)據(jù)流依賴指一個(gè)任務(wù)需要從另一個(gè)任務(wù)那里獲得某些該文介紹的驗(yàn)證方法采用了012中介紹的設(shè)計(jì)( 3455657)理輸入數(shù)據(jù)。論的思想,即根據(jù)給定的輸入條件和一系列運(yùn)算規(guī)則,檢測是對這兩種依賴分析后,可以看出:對于通知依賴,可以用事否可以獲得所需的設(shè)計(jì)。件是否發(fā)生進(jìn)行描述;對于數(shù)據(jù)流依賴,可以用數(shù)據(jù)是否存在一個(gè)設(shè)計(jì)需要至少三種輸入,也被稱作領(lǐng)域描述:或其是否滿足一定條件描述。這樣,就可以用統(tǒng)一的斷言集對 ()初始狀態(tài)的描述;%這兩種依賴進(jìn)行描述。一個(gè)斷言是一個(gè)邏輯表達(dá)式,用來表示( !)目標(biāo)即最終狀態(tài)的描述;某事為

10、真或?yàn)榧?一個(gè)斷言集是一系列邏輯表達(dá)式,從而可以( &)可以被執(zhí)行的動作的描述。用來表示系統(tǒng)中所有事件的真假。這樣一個(gè)任務(wù)可以描述為三設(shè)計(jì)的輸出是一個(gè)動作序列。這些動作在滿足初始狀態(tài)的元式 ( , )。其中, 為其輸入斷言集的集合,表示任! #$ % &$ #$ 條件下執(zhí)行時(shí),最終可以達(dá)到目標(biāo)。這樣,一個(gè)設(shè)計(jì)領(lǐng)域被定義務(wù) !所有可能的輸入斷言集;同樣的,&$為其輸出斷言集的 為不同可能狀態(tài)、可用的動作及由動作執(zhí)行引起的狀態(tài)轉(zhuǎn)換的集合,表示任務(wù) !所有可能的輸出斷言集;%為活動。其中,一語義模型描述。個(gè)輸入斷言集的斷言既可以由一個(gè)前序任務(wù)的某一個(gè)輸出斷這里用 #元組 (*,+,)來描述一個(gè)語義模

11、型。其中,*言集滿足,也可以由多個(gè)前序任務(wù)的多個(gè)輸出斷言集共同滿 是前面提到的斷言的集合,一個(gè)斷言描述了領(lǐng)域的一個(gè)狀態(tài)。足。任務(wù)的執(zhí)行由一個(gè)輸入集的可用性激活。只有第一個(gè)可用由于變量是有限的,依賴是有限的,因此斷言集合必然是有限的輸入集會激活任務(wù)。 的。是 的冪集,它表示狀態(tài)空間。這樣,中的元素就是工作* 圖 !( )描述了工作流的輸入輸出斷言集表示。從圖中可流模式某一時(shí)刻所處的狀態(tài)。+是活動的有限集,它不僅包含以看出,每個(gè)任務(wù)可以有多個(gè)輸入斷言集和多個(gè)輸出斷言集;前面描述的三元式 !(#$,%,&$)中的活動 %,也包括重構(gòu)過一個(gè)輸入斷言集既可以由單個(gè)輸出斷言集滿足 (如 !%+&%,- 程

12、中需要增加的一些偽活動;: 是轉(zhuǎn)換方法。當(dāng) (, -+.$ , /!%#%),也可以由多個(gè)任務(wù)的多個(gè)輸出斷言集滿足(如 !+&%,%)不等于空時(shí),動作 %是可執(zhí)行的,這里 %!+,/!。!&+&%,-!%#!)。當(dāng) #%或 #!中的一個(gè)滿足時(shí),!%任務(wù)就被激 這樣,一個(gè)工作流模式生成問題需要考察一個(gè)三元組(,活。#,!),是 #元組 (*,+,),#89/:是初始狀態(tài),!,是目標(biāo)或終止?fàn)顟B(tài)集。對一個(gè)問題 ;的一個(gè)設(shè)計(jì) 45被定義成&$& 模型重構(gòu), : , , , ,這里 , 被稱作狀態(tài) 活根據(jù)分析,在構(gòu)建工作流模式中,任務(wù)中需要關(guān)注的是其 01%289/ %$ %!+ /! / %$!,: / %$ ,動對。輸入和輸出斷言集,而具體的活動(或操作)只有在實(shí)現(xiàn)的過程在基于設(shè)計(jì)的模型檢查方法中,對一個(gè)設(shè)計(jì)的搜索被形式中才需要考慮。同時(shí),對于連續(xù)的工作流任務(wù),其前驅(qū)任務(wù)的輸出斷言與其后續(xù)任務(wù)的輸入斷言必然具有某種相關(guān)性,即任務(wù) 化為狀態(tài)空間的從終止?fàn)顟B(tài)到初始狀態(tài)的完全搜索。當(dāng)初始節(jié)點(diǎn)通過評估狀態(tài)標(biāo)號被定位時(shí),搜索終止。如果初始節(jié)點(diǎn)能夠之間根據(jù)斷言集進(jìn)行匹配。因此,可以考慮將斷言集表