陳 瑩,孫曉波,邢建春,楊啟亮,2
(1.解放軍理工大學 國防工程學院,南京 210007;2.南京大學 計算機軟件新技術國家重點實驗室,南京 210093)
任務關鍵系統[1](Mission Critical System,MCS)廣泛應用于武器裝備、醫療設備、核電控制、工業控制等諸多國家關鍵信息領域。與傳統安全保障系統相比,MCS不僅可以大大提高系統的安全性,而且能夠滿足特定領域中高可信、高生存以及高可用的要求。但是,盡管已經對MCS的模型進行了防御型建模和驗證分析,該系統也同樣會遭受一定程度的損壞,而且還會導致經濟受到嚴重的破壞[2]。因此,如何保證所有關鍵任務按時完成,并在此基礎上去完成更多的非關鍵任務,是該領域當今急需解決的一個重要問題。
MCS的建模問題本質上是一個工作流的建模問題。目前,工作流的建模技術主要有Petri網[3-4]、進程代數[5]和自動機[6]等方法。從文獻[7]的分析中發現,采用進程代數和自動機的方法對工作流進行建模時,會使模型相對復雜,建模的過程難度也較大。為了使得工作流的建模更簡潔明了,本文采用著色時間Petri網(Colored Time Petri Net,CTPN)對MCS的工作流進行建模。
目前,工作流面臨的重要挑戰是其時間管理問題,工作流管理系統(Work Flow Management System,WFMS)針對該問題并未給出準確的定義。但是,在實際的運用中必須考慮時間約束下工作流的過程管理這一問題。為此,已有很多學者對時間約束驗證進行了不同角度的研究[8]。文獻[9]針對時間推測方法的研究,給出了一套方案。針對一些復雜模型的建模與分析,文獻[10-11]進行了相關研究。文獻[8]提出了一種新的時間約束分析角度,通過引入延遲空間,從而對模型進行時間約束驗證分析。此外,近些年也有一些學者對時間驗證和最優路徑做了相關研究,比如,文獻[12]提出了一種直觀方便的工作流模型靜態時間驗證方法,文獻[13]提出了基于期限的反向優化算法(RRO),該算法通過逆向縮減得到最優路徑。雖然上述研究對時間約束下的工作流過程進行了時間驗證分析[14],但這些方法并不能很好地運用在計算機的運行中[15]。其中很多學者將工作流進行建模和時間驗證,但未將兩者與最優路徑的分析相結合。
基于此,本文將CTPN的建模優勢與工作流相結合[15],建立一個庫所含時間因素的著色時間Petri工作流網(Place Containing the Time factor colored time Petri-Workflow Net,PCTP-WFN),通過對工作流的基本結構進行分析,建立適合其基本結構的時間驗證規則,并在有限時間約束下提出最優路徑的分析策略。
著色時間Petri網是對一般Petri網的擴展,其將Petri網與程序元語言相結合,并以簡潔明了的方式描述并發系統。時間Petri網(Time Petri Net,TPN)的定義由文獻[16]提出,它將一個時間使能區間T[α,β]添加在Petri網中的變遷上,其中,α和β分別表示當變遷t在標識M下具有發生權時t的最早和最晚觸發時間。
目前,由各類含有時間因素的Petri網所建立的模型,一般都是將庫所、變遷以及連接弧賦予時間值[17-19]。然而,變遷遵循瞬間觸發性的原則,如果將時間值賦予在變遷上,便會違背該原則,并且無法用可達標識圖來描述“某一活動正在運行中”這一狀態[20]。針對這一問題,本文運用庫所含時間因素的著色Petri網(Place Containing the Time factor Colored Petri-Net,PCTP-Net)來對工作流過程進行建模與時間驗證。PCTP-Net的具體轉換方式將在第2.3節做詳細介紹。
定義1時間Petri網由一個五元組Σ=(P,T,F,M,I)組成[21]。五元組含義如下:
1)P:描述系統庫所(Place)的有限集合。
2)T:變遷(Transition)的有限集合。
3)F:弧(Arc)的有限集合,滿足F?(P×T∪T×P)。
4)M:P→Z(非負整數集合)是位置集合上的標識向量。
5)I:變遷集合上的時間區間函數T→R0×(R0∪{∞})。
在一般情況下,用橢圓表示庫所,用矩形表示變遷,用有向弧連接庫所和變遷。
定義2一個庫所含時間因素的著色Petri網是一個八元組,PCTP-Net=(P,T,F,C,W,I,M,PT)。八元組含義如下:
1)P:描述系統庫所(Place)的有限集合。
2)T:變遷(Transition)的有限集合。
3)F:弧(Arc)的有限集合[22],滿足F?(P×T∪T×P)。
4)C:色彩集,與每一個庫所和變遷都關聯。具體地說,庫所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維非負整數向量集的映射,即帶顏色的權函數。
6)I:變遷集T向k維非負整數向量集的映射,即帶顏色的標識。
7)M:庫所集P向k維非負整數向量集的映射,即帶顏色的權函數。
8)PT:定義在庫所集上的時間區間函數P→R0×R0,其中,R0表示非負實數集。PT(pj)={T[α1,β1],T[α2,β2],…,T[αk,βk]},是所有庫所的時間間隔,當αk=βk=0時,該值可忽略不寫。
定義3在一個PCTP-Net中,時間間隔[αk,βk]與每個庫所pk都關聯,如PT(pk)=T[αk,βk]。
αk、βk具有如下含義:
1)αk和βk都為已知時間。
2)αk和βk分別為任務執行所需的最小時間和最大時間。
3)若pk的使能時間為一個確定的時間T,則庫所點火時間間隔為T[T+αk,T+βk]。
定義4一個庫所含時間因素的著色時間Petri工作流網是一個九元組:PCTP-WFN=(P,T,F,C,W,I,M0,Ω,PT)。九元組含義如下:
1)(P,T,F,C,W,I,M0,Ω)為一個著色工作流網。
2)PT為定義在庫所集上的時間區間函數P→R0×R0,其中,R0表示非負實數集。
3)M0:P→N0為初始標識。
4)Ω為一系列標識狀態,M∈Ω。
從工作流網(WFN)到PCTP-WFN的映射規則為:當任務的執行時間是唯一確定值d時,則PT(p)=T[d,d],d≥0;當任務的執行時間為變化的時間區間時,PT(p)=T[α,β]。
針對典型Web服務組合工作流的時間管理,文獻[23]給出了在工作流活動中的兩種時間約束:上限約束和下限約束。2個活動間的上限約束是一個有效常數,并且2個活動間的運行時間必須小于該常數。同樣的,2個活動間的下限約束也是一個有效常數,并且2個活動間的運行時間必須大于該常數。該文獻運用時間有向網絡圖(Directed Network Graph,DNG)對工作流進行建模。在工作流的建模過程中,工作流模型一般由TPN來描述,且TPN也常用于時序分析中[24-26]。
在帶有循環的結構中,一些活動會被執行多次,因此,可以用Tck(t)表示活動t循環k次的全局時間。特別情況下,Tc1(t)也可以表示為Tc(t)。
定義5活動ti和活動tj間的上限時間約束為:Tck(tj)-Tck(ti)≤ul,其中,ul為一個有效常數。
活動ti和活動tj之間的下限時間約束為:Tck(tj)-Tck(ti)≥fl,其中,fl為一個有效常數。
TPN在Petri網原型的基礎上定義一個從變遷集到某種時間因素集的映射,這些時間因素表示活動發生所需要的時間或具備觸發條件后實際發生所需要的時間[27]。而Petri網原型根據時間函數(假設為T)的值是否為0,將變遷分為非瞬間變遷和瞬間變遷。從原理上講,這種映射違背了變遷發生的瞬間性原則。因此,為提高Petri網建模的準確性和可行性,本文依照文獻[20]所述,在運用Petri網對模型進行分析時,用一個新的子網來代替一個非瞬間變遷,該子網包括1個帶有時間因素的庫所和2個瞬間變遷,通過對非瞬間變遷的替換得到庫所含時間值的Petri網,從而達到“實際系統運行過程中出現的每一種狀態都可以用模擬它的網系統的一個標識來表示”這一基本要求,最終將CTPN轉換成庫所含時間因素的著色Petri網(PCTP-Net),如圖1所示。

圖1 CTPN向PCTP-Net轉換過程示意圖
MCS的建模問題本質上是一個擴展工作流的建模問題。針對MCS的時間驗證,本文采用PCTP-WFN對系統進行建模。
定義6MCS中的任務分為2種:關鍵任務和非關鍵任務。其中,關鍵任務是為完成最終任務所必須執行的任務,且每個工作流中最少要有一個關鍵任務。
本文假設所有活動都具有正確性。為驗證活動ti至活動tj間的時間約束Tck(tj)-Tck(ti)≤b是否成立,一般情況下,需要找出所有帶活動ti和活動tj的工作流,然后運用傳統的時間驗證方法[24]分別驗證其是否滿足時間約束。但由于TPN同時運行的活動較多,導致工作流路徑的數量呈指數倍增加。因此本文將給出一種實用性和效率都較高的方法對工作流的時間約束進行驗證。
首先通過一個簡單案例來描述工作流時間驗證的方法。時間間隔如圖2案例1中所示,其中,活動t2由t21、p2′和t22所組成,活動t3、t4和t5以此類推。假設活動t1、t2、t3和t6為關鍵任務,如果運用傳統方式[28]驗證上限約束Tc(t6)-Tc(t2)≤6是否滿足,需要驗證4條路徑,使得驗證效率大大減小。由于Tc(t6)-Tc(t2)≤4為上限約束,因此只要驗證Tc(t6)-Tc(t2)是否滿足上限約束即可。由文獻[29]可知,上限約束Tc(t6)-Tc(t2)可等效為Tcmax(t6)-Tcmax(t2),因此,只需要運用遞歸法計算出Tcmax(t6)-Tcmax(t2)的值就可以驗證其是否滿足時間約束: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,故不滿足時間約束。

圖2 案例1
通過上述案例分析可以歸納出計算Tcmax(t)和Tcmin(t)的方法,如定理1所示。
定理1在一個庫所含時間因素的工作流網中,[αi,βi]為活動ti所對應的時間間隔,[α,β]為任一活動t所對應的時間間隔,初始標識為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)=β
證明:對于等式2),庫所pm可能會有多個前驅,pm獲得托肯的最大全局時間為max{Tcmax(pn′)|pn′∈pm},但只有當所有前驅中的托肯都轉移到庫所pm時,活動ti才能被使能,活動ti被使能的最大全局時間為max{max{Tcmax(pn′)|pn′∈pm}|pm∈pi′}。因此,活動ti運行完成的最大全局時間為max{max{Tcmax(pn′)|pn′∈pm}|pm∈pi′}+βi。同理,等式1)也可被證明。
由文獻[25]可知,上限約束和下限約束Tck(tj)-Tck(ti)分別等效于Tcmax(tj)-Tcmax(ti)和Tcmin(tj)-Tcmin(ti)。
利用定理1來驗證時間約束時,為使得驗證簡
單明了,本文通過案例1對定理1進行驗證。圖2中,通過定理1可計算出Tcmax(t6)=8,Tcmax(t2)=3,因此,Tc(t6)-Tc(t2)=5,不滿足時間約束Tc(t6)-Tc(t2)≤4。
對于MCS,在已知的時間約束內,當只執行關鍵任務時,一般會剩有松弛時間,這樣就導致了資源的浪費。因此,本文根據實際情況,將剩余的松弛時間動態地分配給其他非關鍵任務,在滿足時間約束的情況下,盡可能多地執行非關鍵任務,最終選擇出一條最佳路徑。
在描述本文方法前,先舉一個簡單例子進行描述。由于篇幅所限,本節圖中將庫所含時間因素的結構進行隱藏,在圖形上將時間賦予變遷,但本質上每個變遷都是由1個賦予時間值的庫所和2個瞬間變遷所構成。
如圖3的案例2所示,假設活動t1、t4、t5、t10、t11和t14為關鍵任務(用加粗線標注),活動t14到活動t4間的上限時間約束為8 min,即Tc(t14)-Tc(t4)≤8;分別給每個活動的運行時間賦予一個變量xk,即βn-k+1xk,當xk=1時,代表該任務被執行;當xk=0時,代表該任務未被執行。

圖3 案例2
當只執行關鍵任務時,由定理1可得:Tc(t14)-Tc(t4)=Tcmax(t14)-Tcmax(t4)=8-4=4<8,滿足時間約束。為了在滿足時間約束并且剩有松弛時間時能夠執行更多的非關鍵任務,根據不等式求最優解列得如下不等式:
(2x1+ 3x3+2x5+3x7+3x9+2x11+3x13+2x14)-
(2x11+3x13+2x14)≤8
(1)
由于活動t1、t4、t5、t11、t12和t14為關鍵任務,故x1=x5=x11=x14=1,因此式(1)可簡化為:3x3+3x7+3x9≤4。
運用MATLAB進行編程:
clear;∥消除;
v=[3,3,3];∥輸入系數;
k=1;∥擬選取個數;
p=4;∥最優解限定值;
ii=1;
n=length(v);∥v的個數;
C1=n choose k(n,k);∥組合的個數;
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]。
由上述內容可知,在時間約束Tc(t14)-Tc(t4)≤8的情況下,非關鍵任務t6、t8和t12中只能有一個活動被執行,因此,活動t4到活動t14間的最優路徑為t4→t6→t10→t14,或t4→t8→t10→t14,或t4→t10→t12→t14。
通過以上案例分析可以看出本文對于最優路徑選擇的主要思路,其中具體規則如下:
1)順序結構
如圖4所示,活動tj和活動tn之間的時間約束為:
Tc(pn)-Tc(pj)=βn+βn-1+…+βj+1≤bj
則tn到tj之間的時間約束為:
βnx1+βn-1x2+…+βj+1xn-j≤bj,j≥0
2)選擇結構
如圖5所示,活動tj和活動tn間的時間約束計算如下。
(1)當選擇第1條路徑時:
Tc(pn)-Tc(pj)=βn+βn-2+…+βj+2≤bj
則tn到tj之間的時間約束為(j為偶數):
βnx1+βn-2x3+…+βj+2xn-j-1≤bj
(2)當選擇第2條路徑時:
Tc(pn)-Tc(pj)=βn+βn-1+…+βj+2≤bj
則tn到tj之間的時間約束為(j為奇數):
βnx1+βn-1x2+…+βj+2xn-j-1≤bj
3)并行結構
如圖6所示,假設tj、tn為關鍵任務,上限時間約束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為偶數)
(1)當j為偶數且max{X,Y}=X時,Tc(tn)-Tc(tj)=βnx1+βn-1x2+…+βj+1xn-j-βjxn-j-1≤bj
(2)當j為偶數且max{X,Y}=Y時,Tc(tn)-Tc(tj)=βnx1+βn-2x2+…+βj+2xn-j-1≤bj
(3)當j為奇數且max{X,Y}=X時,Tc(tn)-Tc(tj)=βnx1+βn-1x2+…+βj+2xn-j-1≤bj
(4)當j為奇數且max{X,Y}=Y時,Tc(tn)-Tc(tj)=βnx1+βn-2x3+…+βj-1xn-j-2-βjxn-j-1≤bj
由于循環結構可以轉化為順序結構,限于篇幅有限,此處不再贅述。

圖4 順序結構

圖5 選擇結構

圖6 并行結構
為了更好說明文中所提出的時間驗證和最佳路徑選擇方法的實用性,以軍港岸基保障信息系統為例驗證該方法。
軍港碼頭一般設置有食品供應中心、供水中心、
供電中心、供暖中心等岸基保障設施,艦艇靠岸駐泊后,岸基保障部門通過這些保障設施為艦艇補給水、電、氣、食品以及軍械、彈藥等物資[30],該工作流程如圖7所示,圖中灰色部分表示關鍵任務,其他部分表示非關鍵任務,其中分發任務A和分發任務B組成了一個并行結構。

圖7 基本流程
將圖7中的所有任務分別用Petri網中的符號來表示,如圖8所示。圖8中每個活動運行的時間間隔已標出,由圖7可知活動t1、t7、t8、t9、t10、t11、t12、t14為關鍵任務,假設活動t14到活動t1間的上限時間約束為23 min,即Tc(t14)-Tc(t1)≤23,由定義5和定理1對以上時間約束進行運算:
1)根據定理1和并行結構上限時間約束規則,又因為X=Y,所以當j為奇數且max{X,Y}=X=Y時:
Tc(t14)-Tc(t1)=2x1+2x2+4x4+3x6+4x8+
2x10+2x11+x12+3x13≤23
(2)
2)由于活動t7、t9、t11、t14為關鍵任務,即x1=x4=x6=x8=1,因此式(2)可化簡為:2x2+4x8+2x10+2x11+x12+3x13≤10
3)由MATLAB可得式(2)取得最大值的組合為:[x2,x8,x10,x11,x12,x13]=[1,0,1,1,1,1]
因此,在時間約束Tc(t14)-Tc(t1)≤23情況下,最優路徑為:t1→t2→t3→t4→t5→t9→t11→t13→t14。

圖8 案例3
以上運用軍港岸基保障信息系統這一案例對本文時間約束規則進行驗證,并運用MATLAB對路徑組合進行不等式最大值求解,最終得出時間約束下的最優路徑。
本文基于PCTP-WFN對工作流進行建模,首先,將工作流中的任務劃分為關鍵任務和非關鍵任務,通過遞推歸納得出驗證時間約束的規則;然后,運用案例驗證規則的正確性,同時用MATLAB對時間約束的數學模型進行運算分析,從而得出工作流中的最佳路徑;最后,對軍港岸基保障信息系統案例進行分析,結果表明該方法具有一定的實用性和可行性。下一步將在以下方面展開研究:將關鍵任務進行更細致地劃分,使得時間驗證更精確;對時間約束下最優路徑的推理方法進行改進,使得該方法具有通用性和完備性;對任務關鍵系統的資源驗證方法進行研究。
[1] 王 濤.任務關鍵系統的軟件行為建模與檢測技術研究[D].秦皇島:燕山大學,2014.
[2] 李 琳,趙國生.基于Agent的可生存系統認知單元結構模型[J].哈爾濱師范大學自然科學學報,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] 李 丹,陳啟璋,劉 強.一種基于Petri網的時間工作流模型的研究與驗證[J].計算機工程,2007,33(7):78-80.
[13] 羅智勇,汪 鵬,尤 波,等.逆向歸約時間約束工作流準確率優化調度[J].北京郵電大學學報(自然科學版),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網的工作流時間動態預測及驗證[J].計算機測量與控制,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] 林 闖.隨機Petri網和系統性能評價[M].北京:清華大學出版社,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網的Web服務組合時間驗證分析[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] 朱連章,張樂偉,劉璐璐.基于賦時分層著色Petri網的以太網系統建模[J].計算機工程與科學,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網在井下機車調度中的建模與仿真[D].合肥:合肥工業大學,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] 楊啟亮,李決龍,邢建春,等.需求自感知的軍港岸基保障物聯網系統[J].國防科技,2014,35(2):56-62.