任务关键系统的时间约束验证与最优路径分析

陈 莹,孙晓波,邢建春,杨启亮,2

(1.解放军理工大学 国防工程学院,南京 210007;2.南京大学 计算机软件新技术国家重点实验室,南京 210093)

0 概述

任务关键系统[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),通过对工作流的基本结构进行分析,建立适合其基本结构的时间验证规则,并在有限时间约束下提出最优路径的分析策略。

1 相关概念

1.1 着色时间Petri网

着色时间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[α,β]。

1.2 时间约束

针对典型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为一个有效常数。

2 MCS的建模与时间验证

2.1 MCS工作流的执行时间

TPN在Petri网原型的基础上定义一个从变迁集到某种时间因素集的映射,这些时间因素表示活动发生所需要的时间或具备触发条件后实际发生所需要的时间[27]。而Petri网原型根据时间函数(假设为T)的值是否为0,将变迁分为非瞬间变迁和瞬间变迁。从原理上讲,这种映射违背了变迁发生的瞬间性原则。因此,为提高Petri网建模的准确性和可行性,本文依照文献[20]所述,在运用Petri网对模型进行分析时,用一个新的子网来代替一个非瞬间变迁,该子网包括1个带有时间因素的库所和2个瞬间变迁,通过对非瞬间变迁的替换得到库所含时间值的Petri网,从而达到“实际系统运行过程中出现的每一种状态都可以用模拟它的网系统的一个标识来表示”这一基本要求,最终将CTPN转换成库所含时间因素的着色Petri网(PCTP-Net),如图1所示。

图1 CTPN向PCTP-Net转换过程示意图

2.2 基于PCTP-WFN的MCS建模

MCS的建模问题本质上是一个扩展工作流的建模问题。针对MCS的时间验证,本文采用PCTP-WFN对系统进行建模。

定义6MCS中的任务分为2种:关键任务和非关键任务。其中,关键任务是为完成最终任务所必须执行的任务,且每个工作流中最少要有一个关键任务。

2.3 时间验证

本文假设所有活动都具有正确性。为验证活动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。

2.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 并行结构

3 案例分析

为了更好说明文中所提出的时间验证和最佳路径选择方法的实用性,以军港岸基保障信息系统为例验证该方法。

3.1 案例背景

军港码头一般设置有食品供应中心、供水中心、

供电中心、供暖中心等岸基保障设施,舰艇靠岸驻泊后,岸基保障部门通过这些保障设施为舰艇补给水、电、气、食品以及军械、弹药等物资[30],该工作流程如图7所示,图中灰色部分表示关键任务,其他部分表示非关键任务,其中分发任务A和分发任务B组成了一个并行结构。

图7 基本流程

3.2 案例验证

将图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对路径组合进行不等式最大值求解,最终得出时间约束下的最优路径。

4 结束语

本文基于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.