任務(wù)關(guān)鍵系統(tǒng)的時(shí)間約束驗(yàn)證與最優(yōu)路徑分析

陳 瑩,孫曉波,邢建春,楊啟亮,2

(1.解放軍理工大學(xué) 國防工程學(xué)院,南京 210007;2.南京大學(xué) 計(jì)算機(jī)軟件新技術(shù)國家重點(diǎn)實(shí)驗(yàn)室,南京 210093)

0 概述

任務(wù)關(guān)鍵系統(tǒng)[1](Mission Critical System,MCS)廣泛應(yīng)用于武器裝備、醫(yī)療設(shè)備、核電控制、工業(yè)控制等諸多國家關(guān)鍵信息領(lǐng)域。與傳統(tǒng)安全保障系統(tǒng)相比,MCS不僅可以大大提高系統(tǒng)的安全性,而且能夠滿足特定領(lǐng)域中高可信、高生存以及高可用的要求。但是,盡管已經(jīng)對(duì)MCS的模型進(jìn)行了防御型建模和驗(yàn)證分析,該系統(tǒng)也同樣會(huì)遭受一定程度的損壞,而且還會(huì)導(dǎo)致經(jīng)濟(jì)受到嚴(yán)重的破壞[2]。因此,如何保證所有關(guān)鍵任務(wù)按時(shí)完成,并在此基礎(chǔ)上去完成更多的非關(guān)鍵任務(wù),是該領(lǐng)域當(dāng)今急需解決的一個(gè)重要問題。

MCS的建模問題本質(zhì)上是一個(gè)工作流的建模問題。目前,工作流的建模技術(shù)主要有Petri網(wǎng)[3-4]、進(jìn)程代數(shù)[5]和自動(dòng)機(jī)[6]等方法。從文獻(xiàn)[7]的分析中發(fā)現(xiàn),采用進(jìn)程代數(shù)和自動(dòng)機(jī)的方法對(duì)工作流進(jìn)行建模時(shí),會(huì)使模型相對(duì)復(fù)雜,建模的過程難度也較大。為了使得工作流的建模更簡(jiǎn)潔明了,本文采用著色時(shí)間Petri網(wǎng)(Colored Time Petri Net,CTPN)對(duì)MCS的工作流進(jìn)行建模。

目前,工作流面臨的重要挑戰(zhàn)是其時(shí)間管理問題,工作流管理系統(tǒng)(Work Flow Management System,WFMS)針對(duì)該問題并未給出準(zhǔn)確的定義。但是,在實(shí)際的運(yùn)用中必須考慮時(shí)間約束下工作流的過程管理這一問題。為此,已有很多學(xué)者對(duì)時(shí)間約束驗(yàn)證進(jìn)行了不同角度的研究[8]。文獻(xiàn)[9]針對(duì)時(shí)間推測(cè)方法的研究,給出了一套方案。針對(duì)一些復(fù)雜模型的建模與分析,文獻(xiàn)[10-11]進(jìn)行了相關(guān)研究。文獻(xiàn)[8]提出了一種新的時(shí)間約束分析角度,通過引入延遲空間,從而對(duì)模型進(jìn)行時(shí)間約束驗(yàn)證分析。此外,近些年也有一些學(xué)者對(duì)時(shí)間驗(yàn)證和最優(yōu)路徑做了相關(guān)研究,比如,文獻(xiàn)[12]提出了一種直觀方便的工作流模型靜態(tài)時(shí)間驗(yàn)證方法,文獻(xiàn)[13]提出了基于期限的反向優(yōu)化算法(RRO),該算法通過逆向縮減得到最優(yōu)路徑。雖然上述研究對(duì)時(shí)間約束下的工作流過程進(jìn)行了時(shí)間驗(yàn)證分析[14],但這些方法并不能很好地運(yùn)用在計(jì)算機(jī)的運(yùn)行中[15]。其中很多學(xué)者將工作流進(jìn)行建模和時(shí)間驗(yàn)證,但未將兩者與最優(yōu)路徑的分析相結(jié)合。

基于此,本文將CTPN的建模優(yōu)勢(shì)與工作流相結(jié)合[15],建立一個(gè)庫所含時(shí)間因素的著色時(shí)間Petri工作流網(wǎng)(Place Containing the Time factor colored time Petri-Workflow Net,PCTP-WFN),通過對(duì)工作流的基本結(jié)構(gòu)進(jìn)行分析,建立適合其基本結(jié)構(gòu)的時(shí)間驗(yàn)證規(guī)則,并在有限時(shí)間約束下提出最優(yōu)路徑的分析策略。

1 相關(guān)概念

1.1 著色時(shí)間Petri網(wǎng)

著色時(shí)間Petri網(wǎng)是對(duì)一般Petri網(wǎng)的擴(kuò)展,其將Petri網(wǎng)與程序元語言相結(jié)合,并以簡(jiǎn)潔明了的方式描述并發(fā)系統(tǒng)。時(shí)間Petri網(wǎng)(Time Petri Net,TPN)的定義由文獻(xiàn)[16]提出,它將一個(gè)時(shí)間使能區(qū)間T[α,β]添加在Petri網(wǎng)中的變遷上,其中,α和β分別表示當(dāng)變遷t在標(biāo)識(shí)M下具有發(fā)生權(quán)時(shí)t的最早和最晚觸發(fā)時(shí)間。

目前,由各類含有時(shí)間因素的Petri網(wǎng)所建立的模型,一般都是將庫所、變遷以及連接弧賦予時(shí)間值[17-19]。然而,變遷遵循瞬間觸發(fā)性的原則,如果將時(shí)間值賦予在變遷上,便會(huì)違背該原則,并且無法用可達(dá)標(biāo)識(shí)圖來描述“某一活動(dòng)正在運(yùn)行中”這一狀態(tài)[20]。針對(duì)這一問題,本文運(yùn)用庫所含時(shí)間因素的著色Petri網(wǎng)(Place Containing the Time factor Colored Petri-Net,PCTP-Net)來對(duì)工作流過程進(jìn)行建模與時(shí)間驗(yàn)證。PCTP-Net的具體轉(zhuǎn)換方式將在第2.3節(jié)做詳細(xì)介紹。

定義1時(shí)間Petri網(wǎng)由一個(gè)五元組Σ=(P,T,F,M,I)組成[21]。五元組含義如下:

1)P:描述系統(tǒng)庫所(Place)的有限集合。

2)T:變遷(Transition)的有限集合。

3)F:弧(Arc)的有限集合,滿足F?(P×T∪T×P)。

4)M:P→Z(非負(fù)整數(shù)集合)是位置集合上的標(biāo)識(shí)向量。

5)I:變遷集合上的時(shí)間區(qū)間函數(shù)T→R0×(R0∪{∞})。

在一般情況下,用橢圓表示庫所,用矩形表示變遷,用有向弧連接庫所和變遷。

定義2一個(gè)庫所含時(shí)間因素的著色Petri網(wǎng)是一個(gè)八元組,PCTP-Net=(P,T,F,C,W,I,M,PT)。八元組含義如下:

1)P:描述系統(tǒng)庫所(Place)的有限集合。

2)T:變遷(Transition)的有限集合。

3)F:弧(Arc)的有限集合[22],滿足F?(P×T∪T×P)。

4)C:色彩集,與每一個(gè)庫所和變遷都關(guān)聯(lián)。具體地說,庫所pi的色彩集為C(pi)={ai,1,ai,2,…,ai,ui},其中,ui=C(pi),i=1,2,…,n;變遷tj的色彩集為C(tj)={bj,1,bj,2,…,bj,vj},其中,vj=C(tj),j=1,2,…,m。

5)W:有向邊集F向k維非負(fù)整數(shù)向量集的映射,即帶顏色的權(quán)函數(shù)。

6)I:變遷集T向k維非負(fù)整數(shù)向量集的映射,即帶顏色的標(biāo)識(shí)。

7)M:庫所集P向k維非負(fù)整數(shù)向量集的映射,即帶顏色的權(quán)函數(shù)。

8)PT:定義在庫所集上的時(shí)間區(qū)間函數(shù)P→R0×R0,其中,R0表示非負(fù)實(shí)數(shù)集。PT(pj)={T[α1,β1],T[α2,β2],…,T[αk,βk]},是所有庫所的時(shí)間間隔,當(dāng)αk=βk=0時(shí),該值可忽略不寫。

定義3在一個(gè)PCTP-Net中,時(shí)間間隔[αk,βk]與每個(gè)庫所pk都關(guān)聯(lián),如PT(pk)=T[αk,βk]。

αk、βk具有如下含義:

1)αk和βk都為已知時(shí)間。

2)αk和βk分別為任務(wù)執(zhí)行所需的最小時(shí)間和最大時(shí)間。

3)若pk的使能時(shí)間為一個(gè)確定的時(shí)間T,則庫所點(diǎn)火時(shí)間間隔為T[T+αk,T+βk]。

定義4一個(gè)庫所含時(shí)間因素的著色時(shí)間Petri工作流網(wǎng)是一個(gè)九元組:PCTP-WFN=(P,T,F,C,W,I,M0,Ω,PT)。九元組含義如下:

1)(P,T,F,C,W,I,M0,Ω)為一個(gè)著色工作流網(wǎng)。

2)PT為定義在庫所集上的時(shí)間區(qū)間函數(shù)P→R0×R0,其中,R0表示非負(fù)實(shí)數(shù)集。

3)M0:P→N0為初始標(biāo)識(shí)。

4)Ω為一系列標(biāo)識(shí)狀態(tài),M∈Ω。

從工作流網(wǎng)(WFN)到PCTP-WFN的映射規(guī)則為:當(dāng)任務(wù)的執(zhí)行時(shí)間是唯一確定值d時(shí),則PT(p)=T[d,d],d≥0;當(dāng)任務(wù)的執(zhí)行時(shí)間為變化的時(shí)間區(qū)間時(shí),PT(p)=T[α,β]。

1.2 時(shí)間約束

針對(duì)典型Web服務(wù)組合工作流的時(shí)間管理,文獻(xiàn)[23]給出了在工作流活動(dòng)中的兩種時(shí)間約束:上限約束和下限約束。2個(gè)活動(dòng)間的上限約束是一個(gè)有效常數(shù),并且2個(gè)活動(dòng)間的運(yùn)行時(shí)間必須小于該常數(shù)。同樣的,2個(gè)活動(dòng)間的下限約束也是一個(gè)有效常數(shù),并且2個(gè)活動(dòng)間的運(yùn)行時(shí)間必須大于該常數(shù)。該文獻(xiàn)運(yùn)用時(shí)間有向網(wǎng)絡(luò)圖(Directed Network Graph,DNG)對(duì)工作流進(jìn)行建模。在工作流的建模過程中,工作流模型一般由TPN來描述,且TPN也常用于時(shí)序分析中[24-26]。

在帶有循環(huán)的結(jié)構(gòu)中,一些活動(dòng)會(huì)被執(zhí)行多次,因此,可以用Tck(t)表示活動(dòng)t循環(huán)k次的全局時(shí)間。特別情況下,Tc1(t)也可以表示為Tc(t)。

定義5活動(dòng)ti和活動(dòng)tj間的上限時(shí)間約束為:Tck(tj)-Tck(ti)≤ul,其中,ul為一個(gè)有效常數(shù)。

活動(dòng)ti和活動(dòng)tj之間的下限時(shí)間約束為:Tck(tj)-Tck(ti)≥fl,其中,fl為一個(gè)有效常數(shù)。

2 MCS的建模與時(shí)間驗(yàn)證

2.1 MCS工作流的執(zhí)行時(shí)間

TPN在Petri網(wǎng)原型的基礎(chǔ)上定義一個(gè)從變遷集到某種時(shí)間因素集的映射,這些時(shí)間因素表示活動(dòng)發(fā)生所需要的時(shí)間或具備觸發(fā)條件后實(shí)際發(fā)生所需要的時(shí)間[27]。而Petri網(wǎng)原型根據(jù)時(shí)間函數(shù)(假設(shè)為T)的值是否為0,將變遷分為非瞬間變遷和瞬間變遷。從原理上講,這種映射違背了變遷發(fā)生的瞬間性原則。因此,為提高Petri網(wǎng)建模的準(zhǔn)確性和可行性,本文依照文獻(xiàn)[20]所述,在運(yùn)用Petri網(wǎng)對(duì)模型進(jìn)行分析時(shí),用一個(gè)新的子網(wǎng)來代替一個(gè)非瞬間變遷,該子網(wǎng)包括1個(gè)帶有時(shí)間因素的庫所和2個(gè)瞬間變遷,通過對(duì)非瞬間變遷的替換得到庫所含時(shí)間值的Petri網(wǎng),從而達(dá)到“實(shí)際系統(tǒng)運(yùn)行過程中出現(xiàn)的每一種狀態(tài)都可以用模擬它的網(wǎng)系統(tǒng)的一個(gè)標(biāo)識(shí)來表示”這一基本要求,最終將CTPN轉(zhuǎn)換成庫所含時(shí)間因素的著色Petri網(wǎng)(PCTP-Net),如圖1所示。

圖1 CTPN向PCTP-Net轉(zhuǎn)換過程示意圖

2.2 基于PCTP-WFN的MCS建模

MCS的建模問題本質(zhì)上是一個(gè)擴(kuò)展工作流的建模問題。針對(duì)MCS的時(shí)間驗(yàn)證,本文采用PCTP-WFN對(duì)系統(tǒng)進(jìn)行建模。

定義6MCS中的任務(wù)分為2種:關(guān)鍵任務(wù)和非關(guān)鍵任務(wù)。其中,關(guān)鍵任務(wù)是為完成最終任務(wù)所必須執(zhí)行的任務(wù),且每個(gè)工作流中最少要有一個(gè)關(guān)鍵任務(wù)。

2.3 時(shí)間驗(yàn)證

本文假設(shè)所有活動(dòng)都具有正確性。為驗(yàn)證活動(dòng)ti至活動(dòng)tj間的時(shí)間約束Tck(tj)-Tck(ti)≤b是否成立,一般情況下,需要找出所有帶活動(dòng)ti和活動(dòng)tj的工作流,然后運(yùn)用傳統(tǒng)的時(shí)間驗(yàn)證方法[24]分別驗(yàn)證其是否滿足時(shí)間約束。但由于TPN同時(shí)運(yùn)行的活動(dòng)較多,導(dǎo)致工作流路徑的數(shù)量呈指數(shù)倍增加。因此本文將給出一種實(shí)用性和效率都較高的方法對(duì)工作流的時(shí)間約束進(jìn)行驗(yàn)證。

首先通過一個(gè)簡(jiǎn)單案例來描述工作流時(shí)間驗(yàn)證的方法。時(shí)間間隔如圖2案例1中所示,其中,活動(dòng)t2由t21、p2′和t22所組成,活動(dòng)t3、t4和t5以此類推。假設(shè)活動(dòng)t1、t2、t3和t6為關(guān)鍵任務(wù),如果運(yùn)用傳統(tǒng)方式[28]驗(yàn)證上限約束Tc(t6)-Tc(t2)≤6是否滿足,需要驗(yàn)證4條路徑,使得驗(yàn)證效率大大減小。由于Tc(t6)-Tc(t2)≤4為上限約束,因此只要驗(yàn)證Tc(t6)-Tc(t2)是否滿足上限約束即可。由文獻(xiàn)[29]可知,上限約束Tc(t6)-Tc(t2)可等效為Tcmax(t6)-Tcmax(t2),因此,只需要運(yùn)用遞歸法計(jì)算出Tcmax(t6)-Tcmax(t2)的值就可以驗(yàn)證其是否滿足時(shí)間約束:Tcmax(t6)=max{Tcmax(p4′),Tcmax(p5′)}+2=max{Tcmax(p2′)+3,Tcmax(p3′)+4}+2=max{Tcmax(p1′)+6,Tcmax(p2′)+6}+2=Tcmax(p1′)+8=8,Tcmax(t2)=Tcmax(p1′)+3=3,Tcmax(t6)-Tcmax(t2)=8-3=5>4,故不滿足時(shí)間約束。

圖2 案例1

通過上述案例分析可以歸納出計(jì)算Tcmax(t)和Tcmin(t)的方法,如定理1所示。

定理1在一個(gè)庫所含時(shí)間因素的工作流網(wǎng)中,[αi,βi]為活動(dòng)ti所對(duì)應(yīng)的時(shí)間間隔,[α,β]為任一活動(dòng)t所對(duì)應(yīng)的時(shí)間間隔,初始標(biāo)識(shí)為M0,則:

1)Tcmin(ti)=max{min{Tcmin(pn′)|pn′∈pm}|pm∈pi′}+αi,Tcmin(t)=α

2)Tcmax(ti)=max{max{Tcmax(pn′)|pn′∈pm}|pm∈pi′}+βi,Tcmax(t)=β

證明:對(duì)于等式2),庫所pm可能會(huì)有多個(gè)前驅(qū),pm獲得托肯的最大全局時(shí)間為max{Tcmax(pn′)|pn′∈pm},但只有當(dāng)所有前驅(qū)中的托肯都轉(zhuǎn)移到庫所pm時(shí),活動(dòng)ti才能被使能,活動(dòng)ti被使能的最大全局時(shí)間為max{max{Tcmax(pn′)|pn′∈pm}|pm∈pi′}。因此,活動(dòng)ti運(yùn)行完成的最大全局時(shí)間為max{max{Tcmax(pn′)|pn′∈pm}|pm∈pi′}+βi。同理,等式1)也可被證明。

由文獻(xiàn)[25]可知,上限約束和下限約束Tck(tj)-Tck(ti)分別等效于Tcmax(tj)-Tcmax(ti)和Tcmin(tj)-Tcmin(ti)。

利用定理1來驗(yàn)證時(shí)間約束時(shí),為使得驗(yàn)證簡(jiǎn)

單明了,本文通過案例1對(duì)定理1進(jìn)行驗(yàn)證。圖2中,通過定理1可計(jì)算出Tcmax(t6)=8,Tcmax(t2)=3,因此,Tc(t6)-Tc(t2)=5,不滿足時(shí)間約束Tc(t6)-Tc(t2)≤4。

2.4 最佳路徑

對(duì)于MCS,在已知的時(shí)間約束內(nèi),當(dāng)只執(zhí)行關(guān)鍵任務(wù)時(shí),一般會(huì)剩有松弛時(shí)間,這樣就導(dǎo)致了資源的浪費(fèi)。因此,本文根據(jù)實(shí)際情況,將剩余的松弛時(shí)間動(dòng)態(tài)地分配給其他非關(guān)鍵任務(wù),在滿足時(shí)間約束的情況下,盡可能多地執(zhí)行非關(guān)鍵任務(wù),最終選擇出一條最佳路徑。

在描述本文方法前,先舉一個(gè)簡(jiǎn)單例子進(jìn)行描述。由于篇幅所限,本節(jié)圖中將庫所含時(shí)間因素的結(jié)構(gòu)進(jìn)行隱藏,在圖形上將時(shí)間賦予變遷,但本質(zhì)上每個(gè)變遷都是由1個(gè)賦予時(shí)間值的庫所和2個(gè)瞬間變遷所構(gòu)成。

如圖3的案例2所示,假設(shè)活動(dòng)t1、t4、t5、t10、t11和t14為關(guān)鍵任務(wù)(用加粗線標(biāo)注),活動(dòng)t14到活動(dòng)t4間的上限時(shí)間約束為8 min,即Tc(t14)-Tc(t4)≤8;分別給每個(gè)活動(dòng)的運(yùn)行時(shí)間賦予一個(gè)變量xk,即βn-k+1xk,當(dāng)xk=1時(shí),代表該任務(wù)被執(zhí)行;當(dāng)xk=0時(shí),代表該任務(wù)未被執(zhí)行。

圖3 案例2

當(dāng)只執(zhí)行關(guān)鍵任務(wù)時(shí),由定理1可得:Tc(t14)-Tc(t4)=Tcmax(t14)-Tcmax(t4)=8-4=4<8,滿足時(shí)間約束。為了在滿足時(shí)間約束并且剩有松弛時(shí)間時(shí)能夠執(zhí)行更多的非關(guān)鍵任務(wù),根據(jù)不等式求最優(yōu)解列得如下不等式:

(2x1+ 3x3+2x5+3x7+3x9+2x11+3x13+2x14)-

(2x11+3x13+2x14)≤8

(1)

由于活動(dòng)t1、t4、t5、t11、t12和t14為關(guān)鍵任務(wù),故x1=x5=x11=x14=1,因此式(1)可簡(jiǎn)化為:3x3+3x7+3x9≤4。

運(yùn)用MATLAB進(jìn)行編程:

clear;∥消除;

v=[3,3,3];∥輸入系數(shù);

k=1;∥擬選取個(gè)數(shù);

p=4;∥最優(yōu)解限定值;

ii=1;

n=length(v);∥v的個(gè)數(shù);

C1=n choose k(n,k);∥組合的個(gè)數(shù);

C2=n choose k(v,k);∥每種組合的向量;

summa=sum(C2,2) ;∥新生成向量求和;

for i=1:1:C1;

if summa(i)<=p

manzujie(ii)=i;

ii=ii+1;

end

end

由以上程序可求得式(1)的最大值組合,即:[x3,x7,x9]=[1,0,0]或[0,1,0]或[0,0,1]。

由上述內(nèi)容可知,在時(shí)間約束Tc(t14)-Tc(t4)≤8的情況下,非關(guān)鍵任務(wù)t6、t8和t12中只能有一個(gè)活動(dòng)被執(zhí)行,因此,活動(dòng)t4到活動(dòng)t14間的最優(yōu)路徑為t4→t6→t10→t14,或t4→t8→t10→t14,或t4→t10→t12→t14。

通過以上案例分析可以看出本文對(duì)于最優(yōu)路徑選擇的主要思路,其中具體規(guī)則如下:

1)順序結(jié)構(gòu)

如圖4所示,活動(dòng)tj和活動(dòng)tn之間的時(shí)間約束為:

Tc(pn)-Tc(pj)=βn+βn-1+…+βj+1≤bj

則tn到tj之間的時(shí)間約束為:

βnx1+βn-1x2+…+βj+1xn-j≤bj,j≥0

2)選擇結(jié)構(gòu)

如圖5所示,活動(dòng)tj和活動(dòng)tn間的時(shí)間約束計(jì)算如下。

(1)當(dāng)選擇第1條路徑時(shí):

Tc(pn)-Tc(pj)=βn+βn-2+…+βj+2≤bj

則tn到tj之間的時(shí)間約束為(j為偶數(shù)):

βnx1+βn-2x3+…+βj+2xn-j-1≤bj

(2)當(dāng)選擇第2條路徑時(shí):

Tc(pn)-Tc(pj)=βn+βn-1+…+βj+2≤bj

則tn到tj之間的時(shí)間約束為(j為奇數(shù)):

βnx1+βn-1x2+…+βj+2xn-j-1≤bj

3)并行結(jié)構(gòu)

如圖6所示,假設(shè)tj、tn為關(guān)鍵任務(wù),上限時(shí)間約束Tc(tn)-Tc(tj)=Tc(pn′)-Tc(pj′)≤bj,由定理1可得:Tc(tn)=βn+β1+max{βn-1+βn-3+…+βk+1+…+β5+β3,βn-2+βn-4+…+βk+…+β4+β2}=βn+β1+max{X,Y}(j為偶數(shù))

(1)當(dāng)j為偶數(shù)且max{X,Y}=X時(shí),Tc(tn)-Tc(tj)=βnx1+βn-1x2+…+βj+1xn-j-βjxn-j-1≤bj

(2)當(dāng)j為偶數(shù)且max{X,Y}=Y時(shí),Tc(tn)-Tc(tj)=βnx1+βn-2x2+…+βj+2xn-j-1≤bj

(3)當(dāng)j為奇數(shù)且max{X,Y}=X時(shí),Tc(tn)-Tc(tj)=βnx1+βn-1x2+…+βj+2xn-j-1≤bj

(4)當(dāng)j為奇數(shù)且max{X,Y}=Y時(shí),Tc(tn)-Tc(tj)=βnx1+βn-2x3+…+βj-1xn-j-2-βjxn-j-1≤bj

由于循環(huán)結(jié)構(gòu)可以轉(zhuǎn)化為順序結(jié)構(gòu),限于篇幅有限,此處不再贅述。

圖4 順序結(jié)構(gòu)

圖5 選擇結(jié)構(gòu)

圖6 并行結(jié)構(gòu)

3 案例分析

為了更好說明文中所提出的時(shí)間驗(yàn)證和最佳路徑選擇方法的實(shí)用性,以軍港岸基保障信息系統(tǒng)為例驗(yàn)證該方法。

3.1 案例背景

軍港碼頭一般設(shè)置有食品供應(yīng)中心、供水中心、

供電中心、供暖中心等岸基保障設(shè)施,艦艇靠岸駐泊后,岸基保障部門通過這些保障設(shè)施為艦艇補(bǔ)給水、電、氣、食品以及軍械、彈藥等物資[30],該工作流程如圖7所示,圖中灰色部分表示關(guān)鍵任務(wù),其他部分表示非關(guān)鍵任務(wù),其中分發(fā)任務(wù)A和分發(fā)任務(wù)B組成了一個(gè)并行結(jié)構(gòu)。

圖7 基本流程

3.2 案例驗(yàn)證

將圖7中的所有任務(wù)分別用Petri網(wǎng)中的符號(hào)來表示,如圖8所示。圖8中每個(gè)活動(dòng)運(yùn)行的時(shí)間間隔已標(biāo)出,由圖7可知活動(dòng)t1、t7、t8、t9、t10、t11、t12、t14為關(guān)鍵任務(wù),假設(shè)活動(dòng)t14到活動(dòng)t1間的上限時(shí)間約束為23 min,即Tc(t14)-Tc(t1)≤23,由定義5和定理1對(duì)以上時(shí)間約束進(jìn)行運(yùn)算:

1)根據(jù)定理1和并行結(jié)構(gòu)上限時(shí)間約束規(guī)則,又因?yàn)閄=Y,所以當(dāng)j為奇數(shù)且max{X,Y}=X=Y時(shí):

Tc(t14)-Tc(t1)=2x1+2x2+4x4+3x6+4x8+

2x10+2x11+x12+3x13≤23

(2)

2)由于活動(dòng)t7、t9、t11、t14為關(guān)鍵任務(wù),即x1=x4=x6=x8=1,因此式(2)可化簡(jiǎn)為:2x2+4x8+2x10+2x11+x12+3x13≤10

3)由MATLAB可得式(2)取得最大值的組合為:[x2,x8,x10,x11,x12,x13]=[1,0,1,1,1,1]

因此,在時(shí)間約束Tc(t14)-Tc(t1)≤23情況下,最優(yōu)路徑為:t1→t2→t3→t4→t5→t9→t11→t13→t14。

圖8 案例3

以上運(yùn)用軍港岸基保障信息系統(tǒng)這一案例對(duì)本文時(shí)間約束規(guī)則進(jìn)行驗(yàn)證,并運(yùn)用MATLAB對(duì)路徑組合進(jìn)行不等式最大值求解,最終得出時(shí)間約束下的最優(yōu)路徑。

4 結(jié)束語

本文基于PCTP-WFN對(duì)工作流進(jìn)行建模,首先,將工作流中的任務(wù)劃分為關(guān)鍵任務(wù)和非關(guān)鍵任務(wù),通過遞推歸納得出驗(yàn)證時(shí)間約束的規(guī)則;然后,運(yùn)用案例驗(yàn)證規(guī)則的正確性,同時(shí)用MATLAB對(duì)時(shí)間約束的數(shù)學(xué)模型進(jìn)行運(yùn)算分析,從而得出工作流中的最佳路徑;最后,對(duì)軍港岸基保障信息系統(tǒng)案例進(jìn)行分析,結(jié)果表明該方法具有一定的實(shí)用性和可行性。下一步將在以下方面展開研究:將關(guān)鍵任務(wù)進(jìn)行更細(xì)致地劃分,使得時(shí)間驗(yàn)證更精確;對(duì)時(shí)間約束下最優(yōu)路徑的推理方法進(jìn)行改進(jìn),使得該方法具有通用性和完備性;對(duì)任務(wù)關(guān)鍵系統(tǒng)的資源驗(yàn)證方法進(jìn)行研究。

[1] 王 濤.任務(wù)關(guān)鍵系統(tǒng)的軟件行為建模與檢測(cè)技術(shù)研究[D].秦皇島:燕山大學(xué),2014.

[2] 李 琳,趙國生.基于Agent的可生存系統(tǒng)認(rèn)知單元結(jié)構(gòu)模型[J].哈爾濱師范大學(xué)自然科學(xué)學(xué)報(bào),2013,29(6):25-28.

[3] HINZ S,SCHMIDT K,STAHL C.Transforming BPEL to Petri nets[C]//Proceedings of the 3rd International Conference on Business Process Management.Berlin,Germany:Springer,2005:220-235.

[4] MONAKOVA G,KOPP O,LEYMANN F.Improving control flow verification in a business process using an extended Petri net[EB/OL].[2017-03-25].http://www.ceur-ws.org/Vol-438/paper15.pdf.

[5] FERRARA A.Web services:a process algebra approach[C]//Proceedings of the 2nd International Conference on Service Oriented Computing.New York,USA:ACM Press,2004:242-251.

[6] FOSTER H,UCHITEL S,MAGEE J,et al.Model-based verification of Web service compositions[C]//Proceedings of the 18th IEEE International Conference on Automated Software Engineering.Washington D.C.,USA:IEEE Press,2003:152-161.

[7] BREUGEL F V,KOSHKINA M,BREUGEL F V,et al. Models and verification of BPEL[EB/OL].[2017-03-26].http://www.cse.yorku.ca/～franck/research/drafts/tutorial.pdf.

[8] MARJANOVIC O.Dynamic verification of temporal constraints in production workflows[C]//Proceedings of the Australasian Database Conference.Washington D.C.,USA:IEEE Computer Society,2000:341-342.

[9] BETTINI B C,WANG X S,JAJODIA S.Temporal reasoning in workflow systems[J].Distributed and Parallel Databases,2002,11(3):269-306.

[10] AALST W M,HOFSTEDE A H.Verification of workflow task structures:a Petri-net-baset approach[J].Information Systems,2000,25(1):43-69.

[11] AALST W M.Process-aware information systems:lessons to be learned from process mining[C]//Proceedings of Transactions on Petri Nets and Other Models of Concurrency II.Berlin,Germany:Springer,2009:1-26.

[12] 李 丹,陳啟璋,劉 強(qiáng).一種基于Petri網(wǎng)的時(shí)間工作流模型的研究與驗(yàn)證[J].計(jì)算機(jī)工程,2007,33(7):78-80.

[13] 羅智勇,汪 鵬,尤 波,等.逆向歸約時(shí)間約束工作流準(zhǔn)確率優(yōu)化調(diào)度[J].北京郵電大學(xué)學(xué)報(bào)(自然科學(xué)版),2017,40(1):99-104.

[14] LI Huifang,FAN Yushun.Workflow model analysis based on time constraint Petri nets[J].Journal of Software,2004,15(1):17-26.

[15] 譚冠政,肖如健.基于Petri網(wǎng)的工作流時(shí)間動(dòng)態(tài)預(yù)測(cè)及驗(yàn)證[J].計(jì)算機(jī)測(cè)量與控制,2007,15(12):1801-1803.

[16] MERLIN P M.A study of the recoverability of computing systems[D].Berkeley,USA:University of California,1974.

[17] 林 闖.隨機(jī)Petri網(wǎng)和系統(tǒng)性能評(píng)價(jià)[M].北京:清華大學(xué)出版社,2005.

[18] JUAN E Y T,TSAI J J P,MURATA T,et al.Reduction methods for real-time systems using delay time Petri nets[J].IEEE Transactions on Software Engineering,2001,27(5):422-448.

[19] PEDRYCZ W,CAMARGO H.Fuzzy timed Petri nets[J].Fuzzy Sets and Systems,2003,140(2):301-330.

[20] 陳 琨,韓燕波.基于Petri網(wǎng)的Web服務(wù)組合時(shí)間驗(yàn)證分析[J].計(jì)算機(jī)工程與設(shè)計(jì),2007,28(20):4938-4942.

[21] TANG X F.A Petri net-based semantic Web service automatic composition method[J].Journal of Software,2007,18(12):2991-3000.

[22] 朱連章,張樂偉,劉璐璐.基于賦時(shí)分層著色Petri網(wǎng)的以太網(wǎng)系統(tǒng)建模[J].計(jì)算機(jī)工程與科學(xué),2008,30(11):5-8.

[23] EDER J,PANAGOS E,POZEWAUNIG H,et al.Time management in workflow systems[M].Berlin,Germany:Springer,2001:265-280.

[24] YANG Q,CHUANG L,WANG J Y.Linear temporal inference of workflow management systems based on timed Petri nets models[C]//Proceedings of the 1st International Conference on Engineering and Deployment of Cooperative Information Systems.Berlin,Germany:Springer,2002:30-44.

[25] TANG D,LIU D N.Method of reachability analysis in HTPN based workflow model[J].Computer Integrated Manufacturing Systems,2006,12(4):487-493.

[26] SALIMIFARD K,WRIGHT M.Petri net-based modelling of workflow systems:an overview[J].European Journal of Operational Research,2001,134(3):664-676.

[27] 郭智奇.Petri網(wǎng)在井下機(jī)車調(diào)度中的建模與仿真[D].合肥:合肥工業(yè)大學(xué),2007.

[28] CHEN J,YANG Y.Temporal dependency based checkpoint selection for dynamic verification of fixed-time constraints in grid workflow systems[C]//Proceedings of International Conference on Software Engineering.New York,USA:ACM Press,2008:141-150.

[29] TSAI J J P,YANG S J,CHANG Y H.Timing constraint Petri nets and their application to schedulability analysis of real-time system specifications[J].IEEE Transactions on Software Engineering,1995,21(1):32-49.

[30] 楊啟亮,李決龍,邢建春,等.需求自感知的軍港岸基保障物聯(lián)網(wǎng)系統(tǒng)[J].國防科技,2014,35(2):56-62.