有色Petri网论文（精选7篇）
有色Petri网论文 第1篇
Petri网直观的图形表示和严密的数学基础,使得Petri网在系统建模与分析中被广泛应用。但是传统的Petri网具有封闭、状态空间爆炸等缺点,而有色Petri网却能避免状态空间爆炸问题,此外,有色Petri网的层次性也可以有效地降低模型的复杂性。
系统的有色Petri网模型,通常使用由丹麦奥胡斯大学的 “CPN团队”所研发的CPN tools 4. 0来进行动态仿真分析。通过生成的状态空间报告来分析验证系统模型的回归性、有界性、 活性及公平性,通常只有这四个动态特性都满足要求时所建立的CPN模型才是正确的,从而也有效地保证了系统的安全性。
模型检验［2］是自动验证并行系统性质的算法,其思想是使用状态空间查询法来检测某给定计算模型是否满足某个时序逻辑公式所表示出的特定性质。文献[7]利用CPN Tools对电子结算交易系统建模,并进行模型检验,结果表明CPN Tools的存储能力和处理状态空间的能力并比不上其他工具,虽然如此,但是它可以有效地处理特定规模的模型。分支时序逻辑ASK-CTL公式的引用使得CPN Tools集成了更强大的模型检验的功能。Chen L J［6］在验证欧洲火车ETCS( European Train Control Sys- tem) 控制系统中安全通信协议的安全性时,使用状态空间法分析并验证了协议的安全层CPN模型中死标识的合理性。
本文首先根据有色Petri网定义及建模过程,提出基于有色Petri网的建模建立与模型检验算法。针对所建立的CPN模型, 我们采用CPN Tools进行仿真。当状态空间仿真报告显示模型中存在死标识时,采用模型检验理论提出基于ASK-CTL的死标识合理性分析与验证算法来对系统的CPN模型进行检验以确保系统的安全运行。
1有色Petri网概念
1. 1有色Petri网概念
有色Petri网CPN在描述系统的并发、分叉、同步等行为以及处理数据方面具有强大优势,其层次化的概念在大型复杂系统的分析过程中有效的抑制了“状态空间爆炸”问题,并允许建模者通过运用多个相互联系的CPN子模型来对大型复杂系统进行建模,可以有效地减小模型的复杂度,增强系统模型的表达性。
定义1有色Petri网CPN［9］定义为一个九元数组CPN = ( Σ,P,T,A,N,C,G,E,I) ,其中: Σ 为非空类型的有限集,P为库所的有限集,T为变迁的有限集,A为弧的有限集,N为节点函数,C为颜色函数,G为防卫函数,E为弧表达式函数,I为初始化函数。
1. 2 CPN Tools简介
CPN tools是建立、模拟和分析CPN模型的强大工具,它支持状态空间分析、时间仿真分析、功能分析,并且用户可以根据自己的需要在模拟过程中编写自己的程序块去提取性能评价所需要的数据,在实际的系统建模中得到广泛应用。
通常我们利用CPN tools对所建立的模型进行动态分析,通过生成的状态空间报告来分析模型的回归性、有界性、活性及公平性,并由这些性质来验证模型的准确性。
1. 3 ASK-CTL与模型检验
模型检验是一种自动验证有穷状态系统的技术,它可以很快发现设计错误,其基本思想是通过遍历系统模型的状态空间来验证系统的特定性质。本文的特定性质由ASK-CTL公式来表达。
CPN支持分支时序逻辑ASK-CTL公式,能很好地应用于形式化的验证中。但是基于CPN Tools的状态空间分析报告无法提供死标识、死变迁、活变迁的相关信息。因此需要在CPN Tools中使用分支时序逻辑ASK-CTL公式来增强CPN Tools的模型检验功能。
ASK-CTL在工具Design / CPN中被有色Petri网的状态空间( 也称为发生图OG( Occurrence Graph) 、可达图/可达树) 所描述。ASK-CTL的库包含了模型检验器。它以ASK-STL公式为论据,检验与当前状态空间相违背的公式,并返回给定公式的真实值。出于效率原因,一般算法考虑了强连接组分图SCCG ( Strongly Connected Component Graph) 。此外,ASK-CTL与模型检验器都在标准建模语言SML( Standard Modeling Language) 中被补充,查询法也在SML语法中被直接公式化。
由Design/CPN ASK-CTL手册［4］我们知道基于ASK-CTL的模型检测函数语法为:
val eval_node : A - > Node - > bool;
/ / 为节点函数,常用于状态公式化,为模型检测的起点,该函数的返/ / 回值为“true”或“false”。当返回“false”时,函数会给出一个显示反例/ / 的诊断信息。
val eval_arc : A - > Node - > bool;
/ / 为弧函数,常用于变迁公式化,用法类似于节点函数。
在CPN Tools中,常用eval_node( ) 函数实现模型检测,其格式如下:
val eval_node( VALUE self,NODE * node)
其中,self函数是ASK-CTL库中自带的查询函数［5］,比如回归性查询函数Home Marking( ) ,可达性查询函数Reachable( ) / SccReachable( ) / AllReachable( ) 等,self也可以通过SML来编辑相应的功能函数。
在进行死标识枚举时,self采用系统自带查询函数List- Dead Markings( )［5］,List Dead Markings( ) 语法为:
fun List Dead Markings unit - > Node list
List Dead Markings( ) 返回列有所有死标识节点的表单,对于资源分配系统,List Dead Markings( ) 返回空列表。
2算法研究
2. 1有色Petri网模型建立与模型检验算法
根据Kurt Jensen对有色Petri网的定义［9］、Petri网原理［1］及丹麦Aarhus大学CPN团队开发的CPN Tools 4. 0的帮助文件［4］,提出了如图1所示的基于有色Petri网模型建立与模型检验算法。
该算法的输入为需要被建模的系统。根据系统的运行原理确定库所/变迁的含义与数量。按照同类的标记赋予相同的颜色不同的标记赋予不同的颜色的原理对库所颜色进行分类并确定库所的颜色集,然后按照系统的实际运行过程建立系统的CPN模型,确定相应的弧函数,功能函数表达式等。将相应的颜色集、弧函数或功能函数标记在相应的库所/变迁、弧上后,在 “Standard declarations”中声明相应的变量与颜色集。
模型搭建完成后,使用CPN Tools中的仿真工具对模型进行仿真,得到状态空间报告用以分析系统的动态特性,并为进行模型检验做准备。模型检验是一种自动验证有穷状态系统性质的算法,其思想是使用状态空间查询法来检测某给定计算模型是否满足某个时序逻辑公式所表示出的特定性质。
本文针对使用CPN Tools进行仿真所得状态空间报告中出现的死标识是否合理,提出了下节的死标识合理性分析与验证算法。
2. 2有色Petri网模型建立与模型检验算法
首先我们给出死标识、死锁的定义如下:
定义2 ( 死标识)对于CPN = ( ∑,P,T,A,N,C,G,E, M0) ,若M ∈ R( M0) 使得 t ∈ T: ┐ M[t > ,则称M为CPN的一个死标识( Dead Marking) 。
定义3( 死锁)对于CPN = ( ∑,P,T,A,N,C,G,E,M0) ,其中P1∈ P。若*P1P*1,则称P1为CPN的一个死锁( Deadlock) 。
活性［1］的概念的提出源于对实际系统运行中是否会出现死锁的探索的需要。当状态空间报告中存在死标识或者死变迁时,需要分析系统是否存在死锁或活锁。对死锁的分析等价于从死标识中找到死锁标识。活锁检查的目的是为了及时发现系统中存在的死循环。活锁的检查通常是根据状态空间报告中OG和SCCG的节点和弧的是否数量相同来确认。OG中死标识包括正常停止状态和死锁,若OG和SCCG节点和弧的数量相同,即同构［6］的,则系统不存在活锁。只有当系统中同时不存在死锁和活锁时,系统才是安全的。
针对CPN模型中存在的死标识,提出了如图2所示的基于ASK-CTL与模型检验理论的CPN模型中死标识合理性分析与验证算法。该算法仅适用于系统的CPN模型的状态空间报告中出现死标识的情况。
该算法的输入为系统的CPN模型,输出为CPN Tools生成的状态空间报告中死标识的合理性。
当状态空间报告显示存在死标识时,为更加严密的验证死标识的存在,采用非标准状态空间查询法在CPN Tools中按照 “let-in-end”的格式编辑相关功能函数以探索死标识的存在性, 使用ASK-CTL库函数中自带的List Dead Markings( ) 函数对死标识逐一枚举,并根据状态空间报告中OG节点数与SCCG节点数是否相同来判断是否存在活锁。
当验证结果显示确实存在死标识而不存在活锁时,则进入Step4检测系统是否存在自循环终端。死标识不应该包含非法终端,即死锁。自循环终端、非法终端的检测分别使用Out Nodes( ) 、Pre Nodes( ) 函数实现,若Out Nodes( n) = [n],则节点n为自循环节点; 为检测非法终端,Pre Nodes( ) 函数对每个节点进行判断。当Text IO. output返回“No Selfloop Terminal! ” 结果时,表示不存在自循环终端,算法自动进入Step5开始验证系统是否存在死锁。死锁验证采用了Valid Terminal( ) 、 Invalid Terminal( ) 函数实现。当Text IO. output =“No Deadlock Markings! ”时,表示不存在死锁。
只有当系统的CPN模型中同时不存在活锁和死锁时,系统才是安全的,所建立的CPN模型才是正确的。
3电梯门系统建模与仿真
3. 1电梯门系统的CPN模型的建立
电梯门系统含保护装置、开关门机和层门厅门三部分。电梯到达第i层刚停稳门还没来得急打开时,门刀立即插入门锁, 开门机实现开门动作并延时等待上下客服务,服务结束准备关门时,信号装置检查电梯门有无关门中断信号输入。若有,则立即开门并继续等待服务结束; 若无则关门机完成关门过程,门关好后门刀立即拔出门锁,并按照乘客进电梯后设置的指令开始运行。其中关门中断信号主要有: 门系统安全触板是否被按下、 轿厢内或外开门按钮是否被按下、电梯是否超重、其他开门信号。
根据上述电梯门系统运行原理进行颜色集分类与变量声明如图3( c) 所示,按照图1所示的建模算法建立电梯门系统的CPN模型如下图3( a) 所示,各库所/ 变迁的含义如下图3( b) 所示。P1为初始标识,触发变迁T1的发生后进入开门等待状态( P2) ,短暂等待后进入开门过程( T2) ,电梯完全打开( P3) 后进行上下客服务延时( CPN Tools中使用“@ + Td”语句,其中Td为延时时间) 过程,与此同时,电梯系统在进行关门中断信号检测( P4) ,P5为信号检测结束状态,触发变迁T10的发生完成信号检测结果的汇报,延时结束后根据信号检测结果对电梯门进行相应开关门处理。
3. 2电梯门系统的CPN模型状态空间仿真结果
本文根据图1算法建立的图3( a) 所示电梯门系统CPN模型,使用CPN tools 4. 0对其进行500次仿真得到如图4所示的状态空间报告。
图4中有界性显示电梯门系统的CPN模型中各标识均有界,有界性［1］显示了系统对资源的最大与最小需求量,保证了系统的正常运行。关于回归性,图4显示EDS'P1 1为回归标识,即电梯门系统运行能回到初始状态。电梯门系统公平性仿真结果为没有无穷发生序列,反应了电梯门系统各部分在资源竞争中未出现饥饿性问题,对资源的占用是公平的,不存在冲突,系统是公平的。
此外,图4所示的状态空间报告显示该模型中存在49 542个死标识。因此需要使用图2所示的算法对这些死标识进行分析与验证。
4电梯门系统CPN模型检验
图4显示“Statistics”中的“State Space”中OG节点和弧的数量与“Scc Graph”中SCCG节点和弧相应的数量相等,即是同构的,因此该系统的CPN模型中不存在活锁。
按照图2所示的算法过程并参考Design/CPN ASK-CTL手册［4，5］,使用非标准查询法及ML编辑如图5所示的电梯门系统CPN模型中死标识合理性验证算法。
其中,图5上侧分别为死标识枚举算法、自循环终端检测算法、死锁检测算法的具体算法代码,下侧所示为各算法运行得到的结果。
再次编辑函数对死标识进行枚举是为了进一步确认死标识的存在,图5( a) 结果显示使用非标准状态空间查询法得到的死标识枚举结果与CPN Tools运行得到的状态空间报告结果一致,进一步验证了电梯门系统CPN模型中确实有死标识存在。 死标识数量巨大,主要是因为为避免偶然因素造成误差,本实验采用了500次仿真,即电梯门系统的CPN模型在CPN Tools中运行了500次。
图5( b) 的运行结果表明该系统中不存在自循环终端,意味着所有的终端情形都包含在图5( a) 所列的死标识中。也进一步验证了该电梯门系统CPN模型中不存在活锁。
此外,由图3( a) 知,电梯门系统CPN模型使用了4个颜色集。由于颜色集包含的元素越多,存在死锁的可能性越大,因此,图5( c) 的死锁标识检测算法主要分析了颜色集R所包含的4个颜色。图5( c) 的运行结果表明该系统中不存在死锁。
综上,由图4、图5我们知道该电梯门系统CPN模型中既不存在活锁也不存在死锁,因此,图3( a) 所示的电梯门系统CPN模型中的死标识是合理的,即电梯门系统是安全的,所建立的电梯门系统CPN模型是正确的。
5结语
模型检验通过搜索系统模型的状态空间来对系统行为进行验证,其基本思想是通过遍历系统模型的状态空间来检验系统模型是否满足给定的性质,进而实现对模型正确性的验证及系统安全性的保证。
本文主要根据有色Petri网中同类的标记赋予相同的颜色不同的标记赋予不同的颜色的原理提出了基于有色Petri网的建模算法,并对所建立的模型提出了基于ASK-CTL的模型检验方法。 特别针对系统的CPN模型中出现的死标识,提出了基于ASK- CTL及模型检验理论的死标识合理性分析与验证算法。该算法使用ML语言编辑相关功能函数并采用非标准状态空间查询法对存在的死标识进行查询验证,根据查询结果中是否含活锁或死锁来判断死标识的合理性。只有系统的CPN模型中既不存在活锁也不存在死锁时,模型中出现的死标识才是合理的。
最后,本文以电梯门系统为例,按照图1所示的有色Petri网建模算法建立了电梯门系统的CPN模型,为避免偶然因素对实验造成影响,本文采用CPN Tools进行了500次仿真并最终得到如图4所示的状态空间报告。根据状态空间报告分析电梯门系统CPN模型的动态特性,以验证所建立模型的准确性及系统的安全性。针对电梯门系统使用CPN Tools进行仿真发现电梯门系统的CPN模型中存在死标识,我们使用图2所示的基于ASK-CTL的死标识合理性分析与验证算法对死标识进行进一步分析与验证,最终运行结果表明该CPN模型中出现的死标识是合理的。因此本文所建立的电梯门系统的CPN模型是正确的,进而也证明了电梯门系统的安全性。
摘要：针对使用CPN Tools工具建立系统CPN(Colored Petri Net)模型并进行仿真所得到的状态空间报告中出现的死标识是否会影响系统的安全性和模型的正确性进行研究,提出基于ASK-CTL的有色Petri网模型检验算法及死标识合理性验证算法。算法描述了系统有色Petri网的建模与仿真过程,根据得到的状态空间报告判断是否存在死标识,对存在的死标识采用非标准状态空间查询法使用ML语言编辑相关功能函数以验证死标识的合理性,进而确保所建立CPN模型的正确性与系统的安全性。最后,以电梯门系统为例,证明了算法的有效性。
有色Petri网论文 第2篇
数据库管理系统(DBMS)的一个主要功能是进行数据控制,其中并发控制又是数据控制当中的一个重要内容。并发控制要解决的问题就是串行化调度与死锁检测,进而破坏死锁,使系统得以继续运行。通常使用各种协议来对并发事务对数据库的访问进行控制。目前最常用的封锁协议是2PL协议。但是满足2PL协议的调度却有可能会带来死锁和活锁问题。
Petri网是一种能很好地描述和分析验证系统动态性能的工具。研究人员们很自然地用Petri网去描述和学习并发控制系统。如在FMS中,Petri网得到很好的应用。文献[1]通过建立并发事务共享数据资源的普通Petri网模型,探讨了可串行化调度与死锁检测问题,但是当系统涉及的事务与数据资源较多时,所构造的Petri网模型过于复杂,出现状态“爆炸”现象。
1 并发事务带封锁机制的增广有色Petri网模型
本文讨论的数据库系统有n个并发事务iT(1≤i≤n)和m个共享资源Dj(1≤j≤m)。各事务对共享资源的加锁情况用矩阵Ln×m表示元素lij定义如下:
定义1:抑制弧/容许弧
(1)FΙ⊆(P×T)为抑制弧集,FΠ⊆(P×T)为容许弧集,且FΙ∩FΠ=φ,(FΙ∪FΠ)∩F=φ;
(2)W:(FΙ∪FΠ)→{0}。
定义2:设PΙ(PΠ)表示与抑制弧(容许弧)关联的库所之集合,t在M下可使能发生,当且仅当:
若M[t>,则t在M下可以使能发生M[t>M′,则M′的定义是:
2 建立ECPN＿LM模型
定义3:一个描述并发事务竞争共享资源的带封锁机制的扩展有色Petri网是一个九元组:
ECPN_LM=(P,T;F,FΙ,FΠ,C,I-,I+,M)
其中:P是库所的有限集合;T是变迁的有限集合;F=PT∪TP是普通有向弧的有限集合;FΙ是抑制弧集合;FΠ是容许弧集合;C是颜色集合;I-是PT上的负函数;I+是PT上的正函数,它们的规则与含义如下:
P={p d,p er,p ew,p dr,p pr,p pw,p s,p x,p r,p sl,p w,pl},pd是可利用共享资源;per是各事务申请对各共享资源加共享锁情况;pew是各事务申请对各共享资源加排它锁情况;pdr是事务等待读共享资源状态;ppr是事务准备读共享资源状态;ppw是事务准备写共享资源状态;pr是事务读共享资源状态;pw是事务写共享资源状态;psl是第一个事务对同一共享资源加共享锁状态;ps是共享锁;px是排它锁;lp是事务完成读或写操作后离开状态。
T={tdr,t pr,tpw,tdpr,t us,t s,t x,tsu,t rl,twl},tdr是事务进入等待状态;tpr是事务准备读;tpw是事务准备写;tdpr是等待的事务准备读;tus是事务不申请共享锁;ts是事务申请共享锁(第一个对此共享资源加的共享锁);tx是事务申请排它锁;tsu是事务解开共享锁;trl是事务完成读后准备离开;twl是事务完成写后准备离开。
F={(per,tpr),(pew,tpw),(pd,tpr),(pd,tpw),(tpr,pd),(tpw,pd),(tpr,ppr),(tpw,ppw),(ppr,tus),(ppr,ts),(ppw,tx),(ps,ts),(px,tx),(tus,pr),(ts,pr),(ts,psl),(psl,tsu),(tsu,ps),(tx,pw),(twl,px),(pw,twl),(pr,trl),(trl,lp),(twl,lp),(per,tdr),(tdr,pdr),(pdr,tdpr),(tdpr,ppr)}。
FΙ={(ppw,tpr),(pdr,tpr),(ppw,tdpr),(ps,tus),(ppr,tsu),(ppw,tsu),(pew,tsu),(pdr,twl),(per,twl),(pew,trl),(ppw,trl)}。
FΠ={(ppw,tdr),(px,tus),(px,ts),(ps,tx)}。
C={(1T),(2T),…,(nT),(1D),(2D),…,(mD),(R),(W),(1S),(S2),…,(Sm),(X1),(X2),…,(Xm),(Tl1),(Tl2),…,(Tln)},颜色(iT)(1≤i≤n)与各事务相对应;颜色(Dj)(1≤j≤m)与各共享资源相对应;颜色(R)与(W)分别对应读操作和写操作;颜色(Sj)与(Xj)(1≤j≤m)分别对应各共享资源的共享锁和排它锁;颜色(Tli)(1≤i≤n)对应各事务完成读或写离开;颜色(iT,R,Dj)(1≤i≤n且1≤j≤m)表示事务iT读共享资源Dj;颜色(iT,W,Dj)(1≤i≤n且1≤j≤m)表示事务iT写共享资源Dj。
F1=I-(per,tpr/(T i,R,Dj))=(T i,R,Dj),(lij=1,1≤i≤n,1≤j≤m)
F2=I-(pew,tpw/(T i,W,Dj))=(T i,W,Dj),(lij=-1,1≤i≤n,1≤j≤m)
F3=I-(p d,tpr/(T i,R,Dj))=(Dj),(lij=1,1≤i≤n,1≤j≤m)
F4=I-(p d,tpw/(T i,W,Dj))=(Dj),(lij=-1,1≤i≤n,1≤j≤m)
F9=I-(ppr,tus/(T i,R,Dj))=(T i,R,Dj),(lij=1,1≤i≤n,1≤j≤m)
F10=I-(ppr,t s/(T i,R,Dj))=(T i,R,Dj),(lij=1,1≤i≤n,1≤j≤m)
F11=I-(ppw,t x/(T i,W,Dj))=(T i,W,Dj),(lij=-1,1≤i≤n,1≤j≤m)
F12=I-(p s,t s/(T i,R,Dj))=(S j),(lij=1,1≤i≤n,1≤j≤m)
F13=I-(p x,t x/(T i,W,Dj))=(Xj),(lij=-1,1≤i≤n,1≤j≤m)
F17=I-(psl,tsu/(S j))=(S j),(lij=1,1≤i≤n,1≤j≤m)
F21=I-(pw,twl/(T i,W,Dj))=(T i,W,Dj),(lij=-1,1≤i≤n,1≤j≤m)
F22=I-(p r,trl/(T i,R,Dj))=(T i,R,Dj),(lij=1,1≤i≤n,1≤j≤m)
F25=I-(per,tdr/(T i,R,Dj))=(T i,R,Dj),(lij=1,1≤i≤n,1≤j≤m)
F27=I-(pdr,tdpr/(T i,R,Dj))=(T i,R,Dj),(lij=1,1≤i≤n,1≤j≤m)
F5=I+(pd,tpr/(T i,R,Dj))=(Dj),(lij=1,1≤i≤n,1≤j≤m)
F6=I+(p d,tpw/(T i,W,Dj))=(Dj),(lij=-1,1≤i≤n,1≤j≤m)
F7=I+(ppr,tpr/(T i,R,Dj))=(T i,R,Dj),(lij=1,1≤i≤n,1≤j≤m)
F8=I+(ppw,tpw/(T i,W,Dj))=(T i,W,Dj),(lij=-1,1≤i≤n,1≤j≤m)
F14=I+(p r,tus/(T i,R,Dj))=(T i,R,Dj),(lij=1,1≤i≤n,1≤j≤m)
F15=I+(p r,t s/(T i,R,Dj))=(T i,R,Dj),(lij=1,1≤i≤n,1≤j≤m)
F16=I+(psl,t s/(T i,R,Dj))=(S j),(lij=1,1≤i≤n,1≤j≤m)
F18=I+(p s,tsu/(S j))=(S j),(lij=1,1≤i≤n,1≤j≤m)
F19=I+(pw,t x/(T i,W,Dj))=(T i,W,Dj),(lij=-1,1≤i≤n,1≤j≤m)
F20=I+(p x,twl/(T i,W,Dj))=(Xj),(lij=-1,1≤i≤n,1≤j≤m)
F23=I+(p l,trl/(T i,R,Dj))=(T li),(lij=1,1≤i≤n,1≤j≤m)
F24=I+(p l,twl/(T i,W,Dj))=(T li),(lij=-1,1≤i≤n,1≤j≤m)
F26=I+(pdr,tdr/(T i,R,Dj))=(T i,R,Dj),(lij=1,1≤i≤n,1≤j≤m)
F28=I+(ppr,tdpr/(T i,R,Dj))=(T i,R,Dj),(lij=1,1≤i≤n,1≤j≤m)
FΙ1=I-(ppw,tpr/(T i,R,Dj))={(T k,W,Dj)}∩M(ppw),(lij=1,lkj=-1,1≤i,k≤n,1≤j≤m)
FΙ2=I-(pdr,tpr/(T i,R,Dj))={(T k,R,Dj)}∩M(pdr),(lij=lkj=1,1≤i,k≤n,1≤j≤m)
FΙ3=I-(ppw,tdpr/(T i,R,Dj))={(T k,W,Dj)}∩M(ppw),(l ij=1,lkj=-1,1≤i,k≤n,1≤j≤m)
FΙ4=I-(p s,tus/(T i,R,Dj))=M(p s),(lij=1,1≤i≤n,1≤j≤m)
FΙ5=I-(ppr,tsu/(S j))={(T k,R,Dj)}∩M(ppr),(lkj=1,1≤k≤n,1≤j≤m)
FΙ6=I-(ppw,tsu/(S j))=({(T i,W,Dk)}∩M(ppw))∧
({(T i,R,Dj)}∩M(p r)),(lij=1,lik=-1,1≤i≤n,1≤j,k≤m)
FΙ7=I-(pew,tsu/(S j))=({(T i,W,Dk)}∩M(pew))∧
({(T i,R,Dj)}∩M(p r)),(l ij=1,lik=-1,1≤i≤n,1≤j,k≤m)
FΙ8=I-(pdr,twl/(T i,W,Dj))={(T i,R,Dk)}∩M(pdr),(lij=-1,lik=1,1≤i≤n,1≤j,k≤m)
FΙ9=I-(per,twl/(T i,W,Dj))={(T i,R,Dk)}∩M(per),(lij=-1,lik=1,1≤i≤n,1≤j,k≤m)
FΙ10=I-(pew,trl/(T i,R,Dj))={(T i,W,Dk)}∩M(pew),(lij=1,lik=-1,1≤i≤n,1≤j,k≤m)
FΙ11=I-(ppw,trl/(T i,R,Dj))={(T i,W,Dk)}∩M(ppw),(l ij=1,lik=-1,1≤i≤n,1≤j,k≤m)
FΠ1=I-(ppw,tdr/(T i,R,Dj))={(T k,W,Dj)}∩M(ppw),(l ij=1,lik=-1,1≤i,k≤n,1≤j≤m)
FΠ2=I-(p x,tus/(T i,R,Dj))={(Xj)}∩M(p x),(lij=1,1≤i≤n,1≤j≤m)
FΠ3=I-(p x,t s/(T i,R,Dj))={(Xj)}∩M(p x),(lij=1,1≤i≤n,1≤j≤m)
FΠ4=I-(p s,t x/(T i,R,Dj))={(S j)}∩M(p s),(lij=-1,1≤i≤n,1≤j≤m)
3 模型分析与验证
3.1 封锁机制的正确性分析
由ECPN_LM模型可知,对于一个共享资源Dj(1≤j≤m)可有三个状态:无任何操作,被加了共享锁,被加了排它锁。当事务在读预备状态ppr时,如果事务操作满足ts(此时对于共享资源Dj来说,它没有被加排它锁((Xj)∈M(p x)),且没有被加共享锁((S j)∈M(p s))),那么事务申请共享锁(ts使能发生),同时做M(p s)-(S j):代表已对Dj加共享锁。当此事务在读共享资源Dj时,另一事务也进入读预备状态ppr。此时,ts不满足使能条件,而tus使能发生(因为对已加共享锁的资源Dj来说,其它进程可对它进行读操作,而不必再申请锁)。当库所ppr,ppw,pew为空时,代表最后一个读资源Dj的事务离开了且同时符合2PL协议(接下来会谈到)。此时,tsu使能发生,释放共享锁。根据写操作原则,对共享资源Dj的写操作每时每刻都只能有一个,所以当事务iT在写预备状态ppw时,若对想写的共享资源Dj(Dj已加共享锁((S j)∉M(p s)),又或者先前已有事务对Dj加了排它锁((Xj)∉M(p x))),那么tx不能发生。否则tx将使能发生并对资源Dj加排它锁。当iT进入写操作状态pw后,只有符合2PL协议后,twl才使能发生,解开排它锁。
3.2 写者优先分析
在ECPN_LM模型中,当某时刻有事务iT(1≤i≤n)要对Dj(1≤j≤m)进行写操作,此时来到写预备状态,并通过抑制弧抑制后来的想对共享资源Dj进行读操作的事务。若系统内已存在对资源Dj进行读操作的事务((S j)∉M(p s)),那么tx不能发生,只有这些读Dj的事务全部读完并离开((S j)∈M(p s))时,tx才能发生。然后事务iT对资源Dj加排它锁,并且进入写操作pw,而此时其它想对共享资源Dj进行读操作的事务可进入读预备状态ppr并等待共享锁。
3.3 满足2PL协议分析
在ECPN_LM模型中,由FΙ6,FΙ7,FΙ8,FΙ9四条抑制弧来保证调度满足2PL。变迁tsu要想在(S j)(即最后一个事务解除对共享资源Dj所加的共享锁)情况下发生,那么库所pew,ppw中的标识{(T i,W,D j)1≤j≤m且lij=-1}和库所ppr中的标识{(T i,R,D j)1≤j≤m且lij=1}必须被全部移走,即事务iT只有在获得所需的全部锁之后才能解除其对共享资源Dj所加的共享锁。而当tl发生后,事务iT不再有读写操作。同理,变迁twl要想在(Xj)(即事务解除对共享资源Dj所加的排它锁)情况下发生,那么库所per,pdr中的标识{(T i,R,D j)1≤j≤m且lij=1}必须被全部移走,即事务iT只有在获得所需的全部锁之后才能解除其对共享资源Dj所加的排它锁。因此其变迁发生的序列所对应的调度满足2PL。
3.4 系统无活锁分析
在ECPN_LM模型中,若有事务欲对共享资源Dj(1≤j≤m)进行写操作,且此事务已进入写预备状态ppw,那么往后所有欲对共享资源Dj进行读操作的事务将进入等待状态pdr(由抑制弧FΙ1和容许弧FΠ1实现)。当写Dj的事务进入写操作(tx使能发生)时,所有因等待读Dj的等待事务进入读预备状态ppr,且通过抑制弧FΙ2实现先来先服务。注:库所pdr的标识的颜色集按队列排队。
3.5 死锁检测分析
设调度s由RMG(ECPN_LM)中从M到端点M的路径上的变迁列组成的,则s是死锁状态,当且仅当M(p r)≠0或M(pw)≠0。注:可达标识图RMG(ECPN_LM)可由文献[2]中所提到的算法构造。
假设s是死锁状态,说明s中必存在两个以上的事务,它们由于相互拥有对方所需资源的锁而无法运行。
假设数据库系统有两个并发事务(1T,2T),竞争两个共享资源(1D,2D),其中1T要求对资源1D加共享锁,对资源2D加排它锁;2T要求对资源1D加排它锁,对资源2D加共享锁,加锁矩阵为那么按ECPN_LM模型运行至以下任一种情况:
M′((D1)+(D2),0,(T1,W,D2)+(T2,W,D1),0,0,0,0,(X1)+(X2)0,(T1,R,D1)+(T2,R,D2),0,0)
M′((D1)+(D2),(T1,R,D1)+(T2,R,D2),0,0,0,0,(S1)+(S2),0,0,0,(T1,W,D2)+(T2,W,D1),0)
系统出现死锁状态,所以若调度从M到端点M′或者M′的路径上的变迁列组成,则系统会出现死锁状态。
若按ECPN_LM模型运行至以下情况:
M′′((D1)+(D2),0,0,0,0,0,(S1)+(S2),(X1)+(X2),0,0,0,
(Tl1)+(Tl2)),系统不出现死锁状态,所以若调度由从M到端点M′′的路径上的变迁序列组成,则系统不会出现死锁状态,且该调度为可串行化调度。
4 结论
本模型在一定程度上有适用性,但还有很多问题没有解决,如:用户优先级问题,中断处理问题,安全性检测问题,数据恢复问题。所以很多问题还需进一步探讨。
参考文献
[1]HAN Yao-jun.WU Zhe-hui.Petri net-based serializability and deadlock detection in concurrency control of database[A].第十七届全国数据库学术会议论文集[c].保定:河北大学出版社.2000.
[2]韩耀军,蒋昌俊,罗雪梅.数据库系统并发控制的扩展有色Petri网方法[J].同济大学学报(自然科学版).2004.
[3]韩耀军,罗雪梅,蒋昌俊.扩展Petri网在实时数据库并发控制中的应用[J].系统仿真学报.2003.
有色Petri网论文 第3篇
信息技术的发展极大地促进了科技的发展, 同时也带来了日益严重的信息安全问题。操作系统作为计算机系统的底层软件, 其安全直接影响着整个信息系统的安全。换言之, 保障信息安全必须以操作系统的安全为前提条件。Linux是主流实用操作系统中的杰出代表, 其安全实现机制也一直是人们研究的重点。SELinux作为Linux内核中的典型安全增强模块, 其安全加固效果主要取决于相关安全策略的正确配置。但限于安全策略配置工作的规模复杂性, 手工分析和配置太过耗费时间精力。开展SELinux安全策略的辅助配置手段及自动化分析方法与技术的研究非常必要且意义重大。本文基于有色Petri网建立了SELinux安全策略的自动化分析模型, 并用C语言编程实现了相应的原型系统, 同时还给出了测试验证和分析结果。
2 SELinux安全策略及有色Petri网分析法
2.1 SELinux安全策略及现有分析方法
SELinux是美国国家安全局关于强制访问控制的实现机制, 其支持TE、RBAC和MLS (可选) 等三种安全模型。SELinux安全策略的基本元素参表1所示。
allow规则是SELinux安全策略描述主客体访问控制关系的基本语句类型。其一般形式为:allow{type_set}{type_set}:{class_set}{permission_name}。其中, allow是关键字, “:”是约定使用的分隔符, 第一个type_set和第二个type_set分别代表源类型和目标类型, class_set用于指明客体的类别, permission_set则指明了源类型关于目标类型的操作权限。allow规则的含义是:允许源类型对目标类型的特定类别进行指定操作方式的访问。
当前对SELinux安全策略的分析方法主要有访问控制空间分析法、信息流分析法和基于有色Petri网的分析法。访问控制空间分析法由Jaeger在文献[1]中首先提出, 该方法基于安全策略配置完成各主体访问控制空间的划分来实现安全策略的自动化分析。J.Guttman在文献[2]中, 将主客体和信息流定义为不同的集合对象和相互之间的状态的转化, 给出了信息流分析法的基本方案。文献[3-5]则综合运用访问控制空间分析法和信息流分析法设计和实现了SELinux安全策略的有效性分析和完整性分析。必须指出, 访问控制空间分析法的关注焦点在于单个主客体的访问控制规定是否存在冲突或不一致。对于多个相关主客体的复杂访问控制关系 (如包含中间类型或过滤类型的访问控制关系) 的分析或者从类型级别来检查安全策略配置是否违背安全目标的情形, 则需要采用通配符且须经多次单一主客体访问控制关系的分析方可完成。传统的信息流分析法一般需要对信息流进行完整的描述, 对于指定较少关键中间类型的访问控制关系的分析而言比较繁琐。基于有色Petri网的安全策略分析方法本质上是一种信息流分析法, 文献[6][7]采用有色Petri网并分别基于XML文档和CPN Tools中间文档对SELinux安全策略进行了描述和分析。本文试图完成SELinux安全策略基本元素的自动提取, 并在此基础上实现有色Petri网的自动化构造与分析, 以改善和提高相关方法的自动化程度。
2.2安全分析目标及其描述
安全策略配置关键在于应满足安全需求和安全设计目标, 所以SELinux安全策略分析应着眼于检查当前安全策略配置是否满足安全设计目标, 也即所谓的有效性分析。安全设计目标可通过一组查询语句来具体描述, 并提交给安全策略分析系统进行验证和确认。为方便和规范描述, 并可基于巴科斯范式来形式化查询语句。如表2所示。
2.3有色Petri网分析模型
有色Petri网区别于其它Petri网的最主要区别在于其引入了颜色集的定义[8], 而颜色集把Petri网中出现的数据划分成若干不同的类型。为方便SELinux安全策略的自动化分析, 可将有色Petri网定义为一个九元组<∑, P, T, F, NF, CF, GF, FE, IE>, 具体组成元素物理含义参表3所示。
其间, 两个类型库所之间一般经由权限库所及两个变迁相连接, 表示前一个类型库所对后一个类型库所拥有对应权限库所所代表的访问权限。显然, 这与SELinux安全策略配置中的allow语句完全一致。为此, 基于有色Petri网的SELinux安全策略分析模型的构建将主要基于allow语句的分析和处理来完成。
令牌是库所中的动态对象, 可以从一个库所移动到另一个库所。当且仅当库所中的令牌值和有向弧上的描述一致并通过变迁上的警戒函数测试时, 就可以发生一次变迁。在查询分析过程中, 令牌将记录从查询语句的源类型所对应的库所到当前库所的信息流路径上 (不妨简称为查询信息流路径) 的所有类型信息、权限信息以及查询相关的其它信息, 故可用一个四元组
伴随查询分析过程的向前推进, 查询分析路径上各库所中的令牌值应及时进行调整。具体而言, 首先把当前库所中的令牌值赋值给其所有后继库所的令牌, 然后针对不同的后继库所分别对其令牌值做相应的调整。
3原型设计与实现
3.1总体设计
根据SELinux安全策略配置文件和上述模型, 可实现安全设计目标的有效性分析。具体过程如图1所示。
3.2安全策略要素提取
安全策略要素提取模块直接针对的处理对象是SELinux安全策略配置文件, 从中提取包括类型、属性、类别、权限以及访问控制规则 (主要是allow语句) 等在内的基本元素。其处理步骤有几个。
(1) 分析安全策略配置文件, 并将class、permission、type、attribute、allow、bool、typeattribute的声明语句 (行) 保存到临时文件。其间, 基于接口的声明语句应根据相关接口定义替换为实际对应的策略语句后再进行保存。
(2) 针对步骤1生成的临时文件, 就类型、属性、类别、权限等要素分别提取处理, 并保存到相应结构体中。特别地, allow语句需分解和提取出源类型、目标类型及权限类型, 而根据typeattribute语句可建立type和attribute之间的双向映射。
(3) 针对步骤2得到的allow语句处理结果, 依次检查相应allow规则的源类型和目标类型, 将所有allow规则的源类型和目标类型转换为type, 并过滤掉无效的allow语句。进一步讲, 若allow规则的源类型 (或目标类型) 为attribute, 则基于attribute和type之间的双向映射关系将对应规则转换为相应type源类型 (或目标类型) 的allow规则。同时, 把拥有既非type也非attribute的源类型或目标类型的allow规则抛弃和删除。
3.3有色Petri网构建
基于allow规则语句构建SELinux安全策略有色Petri网模型的基本方法如下:
(1) 将allow规则的源类型和目标类型转化为有色Petri网中的类型库所;
(2) 将allow规则的权限转化为有色Petri网中的权限库所;
(3) 根据allow规则在类型库所和权限库所之间设立access变迁和将它们连接起来。
图2所示为两条allow规则示例及其转化得到的有色Petri网结果。
allow student_t accessrecord_t process{transition};
allow accessrecord_t courserecord_t:file{write};
为利用前述有色Petri网模型验证SELinux安全策略配置关于安全设计目标的有效性, 需提示安全管理人员输入一系列查询语句, 而每次查询处理也需将对应查询语句转化和插入到基于SELinux安全策略配置的allow规则集生成的有色Petri网分析模型中。具体而言, 首先从查询语句中提取出源类型、目标类型、过滤类型、直接/间接信息流标记、读/写信息流访问方式, 然后在有色Petri网分析模型中建立源类型、目标类型以及过滤类型所对应的类型库所。为方便后续的查询处理, 这里对类型库所的标记进行了更为细致的分类处理。譬如, 对于如下的查询语句:teacher_t: (WL, +, ! (collegeadmin_t) ) :courserecord_t
在转化和插入分析模型时, 可将teacher_t、courserecord_t、collegeadmin_t所在库所的分类标记分别设置为Source Type、Target Type和Not List Type。同时, 将分析模型中非上述情况的类型库所的分类标记设置为Ordinary Type, 而将权限库所的分类标记设置为Permission Type。
3.4有色Petri网查询处理
在建立和生成SELinux安全策略有色Petri网模型的基础上, 初始化设定Source Type所在库所的令牌值, 就可启动查询处理过程。
查询处理的实现过程主要涉及由即将处理的相关库所构成的一个库所队列的维护操作。其基本流程如下所述:
其间, 库所v的令牌值更新和设置操作尤为关键, 详细更新方案参表4所示。
针对以上SELinux安全策略分析方法, 基于C语言对进行了实现, 文献[6][7]分别采用CPN Tools和中间XML文档进行了分析。本文采用C语言模拟CPN的执行, 自动化地将访问控制关系及查询语句转化成CPN, 并自动执行变迁, 从而实现了SELinux的安全策略自动化分析。
4原型测试及结果分析
本文基于一个学生-教师系统SELinux应用实例对实验原型进行了测试验证和分析。
4.1测试用例
SELinux应用实例中主要提供了学生选课及教师评分两种服务操作, 系统中的主体类型有三种, 学生类型 (student_t) 、教师类型 (teacher_t) 和管理员类型 (collegeadmin_t) , 客体类型分为学生作业文件类型 (coursework_t) 、选课记录文件类型 (courserecord_t) 、课程资源类型 (coursesourse_t) 、初始成绩类型 (coursepremark_t) 和最终成绩类型 (coursemark_t) , 教师提交初始成绩, 由管理员根据初始成绩得出最终成绩。学生具有读取课程资源、读取最终成绩、写入选课记录以及写入作业文件的权限;教师的权限有读取选课记录、读取学生作业、写入课程资源、写入初始成绩的权限;管理员有读取选课记录、读取课程资源、读取学生作业的、读取始成绩、写入最终成绩的权限。
4.2测试验证
根据3.2节方法提取出allow语句, 选取了两个比较典型的配置语句验证, 在配置语句中有allow student_t accessrecord_t:process transition;allow accessrecord_t courserecord_t:file{write};表示student_t能通过accessrecord_t来最终访问courserecord_t, 采用“正”描述表示为必须有一条从student_t到courserecord_t的信息流;在设计用例时, 不允许teacher_t直接对courserecord_t进行访问, 只能通过collegeadmin_t对courserecord_t进行访问, 采用“负”描述查找teacher_t对courserecord_t进行访问且没经过collegeadmin_t的非法信息流。验证结果如表5所示。
4.3结果分析
在4.2节的验证中给出了两条比较典型的验证语句, 分别从查找合法非法信息流方面对用例中的安全设计目标进行了验证, 结果发现符合了“学生能写课程记录”和“教师不能直接写分数记录”的安全设计目标, 另外对其他的学生、教师、课程记录、作业记录、分数记录直接的访问控制关系设计目标也进行了验证, 由于篇幅关系不再列出, 它们之间的访问关系也符合用例的设计目标, 以上分析说明分析工具能对安全策略进行有效性分析, 同时验证了策略配置的正确性。
5结束语
本文基于有色Petri网设计和实现了SELinux安全策略的自动化分析原型, 解决了验证SELinux安全策略配置正确性的问题。原型测试结果表明, 有色Petri网分析模型可有效描述SELinux安全策略中的访问控制关系, 而对应于安全设计目标描述的方便规范的查询语句通过引入带有中间过滤类型的信息流可支持较为复杂的访问控制关系的分析处理。总体上来讲, 相关分析方法和原型可满足安全策略有效性分析基本要求, 但相关实现细节需要进一步优化和改进。
参考文献
[1]T.Jaeger, X.Zhang, and A.Edwards, Policy management using access control spaces, ACM Transations on Information and System Security.2003, 6 (3) :327-364,
[2]J.Guttman, A.Herzog, and J.Ramsdell, “Information flow in operating systems:Eager formal methods, ”in workshop on Issues in the Theory of Security (WITS) , 2003.
[3]Gaoshou Zhai, Tong Wu, Jing Bai, Tao Guo and Tianyou Li, Algorithms for Automatic Analysis of SELinux Security Policy, International Journal of Security and Its Applications, 2013, Vol.7, No.1, pp.71-84.
[4]Jing Bai, Gaoshou Zhai, Study On Analysis For SELinux Security Policy, Proceedings of 2012 International Conference on Systems and Informatics (ICSAI 2012) , pp.1231-1235.
[5]Gaoshou Zhai, Wenlin Ma, Minli Tian, Na Yang, Chengyu Liu, Hengsheng Yang, Design and Implementation of a Tool for Analyzing SELinux Secure Policy, ICIS 2009, November 24-26, 2009 Seoul, Korea, pp.446-451.
[6]Chen Yi-Ming, Kao Yung-Wei, “Information flow query and verification for security policy of Security-Enhanced Linux, ”Proceedings of the 1st International Workshop on Security (IWSEC 2006) Kyoto, JAPAN, OCT 23-24, 2006, pp.389-404.
[7]Ahn Gail-Joon, Xu Wenjuan, Zhang Xinwen, “Systematic policy analysis for high-assurance services in SELinux, ”Proceedings of the IEEE International Workshop on Policies for Distributed Systems and Networks Palisades, NY, JUN 02-04, 2008, pp.3-10.
有色Petri网论文 第4篇
关键词：SOA,MDA,有色Petri网,服务组合
1 引入基于SOA的MDA开发框架
软件开发方法经历了不断变更,虽然在一定程度上缓解了开发过程中的问题,但不能从根本上解决需求变更、软件移植、软件复用、互操作性及开发效率等问题。此时,模型驱动开发方法便应运而生。对象管理组织提出的MDA(Model Driven Architecture,模型驱动构架)是一个软件开发框架,是一种面向对象模型的软件开发方法。重要的是,模型不再只是文档。模型比代码更有价值,同时模型将被精确地定义,以便代码转换。所以创建出具有复用价值的模型是MDA的开发的关键。
然而,MDA虽有好处,但它在建模阶段的业务模型设计中,没有充分地考虑到业务模型的通用性。当需要对部分或整个业务进行某种形式的更改时,它们就显得非常脆弱,往往需要修改大部分模型,使得模型的通用性以及可重用性大打折扣。而SOA(Service Oriented Architecture,面向服务架构)的面向服务思想则正好弥补了MDA的这种缺陷,使MDA的业务模型由细粒度的基础服务模型组合而来。从而减少了因为业务修改而带来的修改模型的代价,提高了模型开发的效率以及模型可重用性和可维护性。
这就需要,提出一种基于SOA的模型驱动快速开发架构(SOA-based Model-driven Rapid Development Architecture,SMRDA)如图1所示[1],以面向服务的体系结构作为基础,屏蔽环境本身的异构性,并使用分层建模的MDA作为整个开发过程的核心驱动,以此提高系统的开发效率,降低应用的移植和维护成本。
在业务流程层创建合理的可验证的流程服务是文中的研究关键,其他不再赘述。面向服务架构(SOA)具有平台无关、松散耦合等特点,所以适合在互联网这种异构、开放的环境下发布和使用。而在构成复杂的服务时,需要将已有的服务进行正确的组合。因此,如何正确地组合服务成为有效利用这些服务的关键。为此,根据服务组合过程中的逻辑结构,文中定义了服务组合的5种基本结构,并提出了通过这些结构形成的服务的性质及组合服务的构造方法。
2 基于有色Petri网的服务组合模型
2.1 SOA基础服务概念
服务是整个SOA实现的核心。SOA架构的基本元素是服务,SOA指定一组实体,这些实体详细说明了如何提供和消费服务。遵循SOA观点的系统必须要有服务,这些服务是可互操作的、独立的、模块化的、位置明确的、松耦合的并且是可以通过网络查找的。服务是可以组合的,这是服务的一个重要特征。它由下列性质所决定:
(1)服务的封装。
将服务封装成用于业务流程的可重用组件的应用程序函数。它提供信息或简化业务数据从一个有效的、一致的状态向另一个状态的转变。封装隐藏了复杂性。服务的API保持不变,使得用户远离具体实施上的变更。
(2)服务的重用。
服务的可重用性设计显著地降低了成本。为实现可重用性,服务只工作在特定处理过程的上下文中,独立于底层实现和客户需求的变更。
(3)服务的互操作。
互操作并不是一个新概念。在CORBA、DCOM、webSevrcie中就已经采用互操作技术。在SOA中,通过服务之间既定的通信协议进行互操作。主要有同步和异步两种通信机制。SOA提供服务的互操作特性更利于其在多个场合被重用。
因此,SOA的服务需要一种具有异步和并发的特点、形式化的语义及图形化的表示,这样就可以进行模型的简化与验证。而有色Petri网通过采用着色Token的方法,使有色Petri网可以完整地描述服务模型,因而做服务的组合和分析[3]。
2.2 有色petri网基本概念
定义1 有色Petri网(Colored Petri Net,CPN)是一个七元组CPN=(∑,P,T,F,E,C,G),其中(P,T,F)为一个网:
∑是类型的非空有限集,也称为颜色的非空有限集。文中颜色集若无特殊说明,则统一使用此处的∑,不再声明;P为有限状态库所集;T为有限变迁库所集;F为有限弧集F∈(P×T)∪(T×P);E为弧函数,E:F→Boolexpression,表示一个弧到一个布尔表达式的映射,其中,E表示调用服务时输入、输出的参数;C为颜色函数,C:P→∑,C(p)表示p中的颜色类型属于∑;G为哨函数,G:T→Boolexpression,其中,G表示调用一个服务时除输入外要满足的条件。
2.3 服务与Petri网的融合为服务网模型
文中主要讨论服务的内部结构,因此对用于服务发现和服务调用的信息不再赘述。而对于主要的服务网模型,定义如下:
定义2 一个服务的服务网SN(Services Net)的CPN 模型为SN=(∑,P,T,F,E,C,G,In,Out),其中:
(∑,P,T,F,E,C,G)为一个CPN;In为服务的输入库所,其中,∀x∈P∪T:(x,In)∉F,表示没有前集;Out为服务的输出库所,其中,∀x∈P∪T:(Out,x)∉F,表示Out没有后集。
定义3 基本服务具有原子性,即不能再分,只需调用自身的功能便可完成任务,它是组成服务的基础。对于基本服务S,可以构造其CPN 模型SN=(∑,P,T,F,E,C,G,In,Out),如图2所示,其中:P={In,Out};T={service};F={〈In,service〉,〈service,Out〉};E={E〈In,service〉,E〈service,Out〉};C={C(In),C(Out)};G由该服务的语义而定。
定义4 通过调用原子服务,完成自身提供功能的服务称为组合服务。设两个基本服务S1、S2,其中,SN1=(∑,P1,T1,F1,E1,C1,G1,In1,Out1),SN2=(∑,P2,T2,F2,E2,C2,G2,In2,Out2)。基本服务只有一种基本结构,而组合服务包括4种:
(1)顺序组合服务,如图3所示,操作符为“+”,S=S1+S2。
(2)并发组合服务,如图4所示,操作符“
(3)循环组合服务,如图5所示,操作符“μ”,S=μS1。
(4)选择组合服务,如图6所示,操作符
图6 选择组合服务CPN模型
性质1 设有服务S1、S2、S3,则在上运算的代数性质有:①(S1+S2)+S3≅S1+(S2+S3);
对于性质中的式(1),可以做出其CPN模型的可达标识图,可知其在相同的初始标识下可以到达相同的终止标识集,故该式成立。其余公式可同样证明。因此,使用上述公式可以对组合服务进行化简,减小其CPN 模型的规模,从而降低复合服务的复杂度。
性质2
(1)如果一个变迁的每个输入库所都拥有令牌,该变迁即为被允许。一个变迁被允许时,变迁将发生,输入库所的令牌将被消耗,同时为输出库所产生令牌。对于基本服务,只要开始库所中含有令牌,则一定能够引发变迁,无论服务执行成功与否,最后都会得到输出,显然结论就成立了。
(2)对于经过{+,|,||,μ}的一步运算得到的服务,以顺序结构为例如图3所示,设两个基本服务S1、S2,由(1)可知若初始标识为非死标识,则S1 可触发。若正常执行结束,则生成调用服务S2的初始条件,服务S2被触发后进入终止状态;若服务S1执行失败,则直接进入终止状态。因此,对于顺序结构,结论显然成立。对于其他结构可同样证明结论成立。
(3)对经过{+,|,||,μ}的多步复合运算得到的服务,可以使用数学归纳法进行证明。对于基本服务进行{+,|,||,μ}的一步运算,结论成立。设对于经过n步复合的服务结论成立,则经过n+1步的复合运算可以看做两个复合服务的一步运算,由(2)可知,对于一步运算,结论成立。因此,对于n+1步的复合运算得到的服务结论成立,故对于多步复合运算结论成立。
3 实例建模
例如,一个毕业生要找工作,由于各种原因只在南京、宁波两个城市找。他个人更倾向于在宁波签约,但是宁波的公司如果达不到他能在南京所得月薪的60%,他就会在南京签约。需要咨询两地公司的所能提供的月薪,经过对比后再判断去哪里的公司。将这个活动看成一个组合服务S,则一共有4个基本服务,即S1:向南京公司咨询所能得到的月薪;S2:向宁波公司咨询所能得到的月薪;S3:对比月薪;S4:签约。
分析可知,S1、S2两个服务为并发逻辑,它们与S3为顺序逻辑,而S3 和S4为顺序逻辑。因此,S可以表示成S=(S1S2)+S3+S4。其CPN图,如图7所示。
可达标识图是一种简单并且有效的方法,它适用于有界的Petri网,鉴于文中服务组合的有界性,因此可以用可达图来分析。上例的可达图,如图8所示[6]。
(1)开始标识M0和结束标识M4是相连的,且M4没有出度,故该组合服务是可以终止的。
(2)该组合服务中的每个状态都是有界的,因此,该组合服务有界且该组合服务是安全的。
(3)从开始标识M0到结束标识M4总能找到一个变迁序列使得从初始状态到达终止状态,故不存在死锁。从以上分析可知,该组合服务是正确、可终止的。
4 结束语
SOA与MDA的结合是现代软件开发理论与方法的主要发展趋势。为实现两者的最佳结合,给异构系统交互提供理想的解决方案,文中在提出架构技术的基础上,定义了5种服务组合逻辑结构,叙述了通过这些逻辑结构组合而成的服务的性质,并对这些性质进行了简要证明,最后通过一个实例说明了文中提出的结构是正确的。
参考文献
[1]盛津芳,文春艳,王斌.一种基于SOA的模型驱动快速开发架[J].计算机应用于研究,2010,27(3):3763-3766.
[2]Gartner.Service-oriented architecture scenario[M].Amer-ica:Gartner,2003.
[3]钱柱中,陆桑璐,谢立.基于Petri网的Web服务自动组合研究[J].计算机学报,2006,29(7):1057-1062.
[4]OASIS.Mapping of W3C Web service architecture work to SOA RMWork[M].America:OASIS,2005.
[5]OASIS.SOA reference model position paper[M].America:OASIS,2003.
Petri网研究现状综述 第5篇
Petri网首先由著名数学家Carl Adam Petri提出,主要用于刻画计算机系统异步通讯。此后,国内外研究学者对其研究发展做出了大量的工作,基于不同应用场景,加入不同限制条件,从层次、时间、有色等方面对丰富Petri网,形成高级Petri网理论体系。[1][2][3][4][5]高级Petri网可以处理数据、时间、形态等约束条件,能广泛应用于各种领域。
谓词Petri网系统的提出简化了Petri网;模糊Petri网理论中则融合了Petri网与模糊数学;随机Petri网通过随机过程工具可以解决包含随机过程的Petri网问题。
二、Petri网理论基础
Petri网是一种图形化建模工具,有坚实的数学理论支撑,成熟的图形分析技术,强大的仿真工具。Petri网基于过程,可分析复杂系统,表达能力丰富,语义语法精确,数学过程严谨,对于随机系统可以很好地解析。
Petri网可模拟实际系统,分析实际系统的性能和效果,具有网系统的一些性质,即动态性质。可达性、有界性、安全性、活性、可逆性等为Petri网的动态性质。
(一)可达性
作为Petri网最基本的行为特征,由可达性定义可以推导Petri网其余性质。可达性指出,对于一个给定的Petri网,由初始状态可以到达哪些状态,这种到达可以是通过激发一系列的迁移实现的。
(二)有界性
有界性需要我们去确定Petri网中的库所或者资源的容量是否溢出,是检查系统是否存在溢出的有效方法。
(三)安全性
Petri中的库所不会重复启动一项正在进行的操作。
(四)活性
计算机操作系统中,由于对有限的资源基于不合理的策略进行分配,会产生死锁。死锁问题对Petri网是非常重要的,反映了Petri网的活性。
(五)可逆性
能自动从差错中恢复,即自身初始化的Petri网是可逆的,系统不需要人工干预即可恢复。
三、高级Petri网系统(HLPN)
对于系统中的异步、冲突、并发等复杂情况,作为一种强有力的模型分析工具,直观地表示图形,Petri网可以很好地刻画。随着应用的发展,为了增强Petri网的描述能力,众多学者提出了高级Petri网系统(HLPN),比如着色Petri网、赋时Petri网、随机Petri网、谓词Petri网、模糊Petri网。
(一)赋时Petri网
普通Petri网没有考虑时间的因素,而在实际生产过程中,时间因素不可忽视。赋时Petri网通过引入时间扩大Petri的适用范围。赋时变迁Petri网、赋时位置Petri网、赋时弧Petri网均为扩展的赋时Petri网。
(二)着色Petri网
着色Petri网引入标识颜色,将库所中的标识与某种标识符号“颜色”联系,用<库所、标识颜色>对表示信息。着色Petri网可准确描述系统的资源情况、系统的活动和约束,能作为准确表达FMS系统动态行为的模型工具。
(三)谓词Petri网
在各有向边上标注谓词,该谓词不直接规定网络的运行,通过对变量的赋值确定某个标识下,哪些变迁可以发生、该变迁对标识变化的影响,谓词Petri网提高了系统的模拟能力。目前,电力行业的系统模拟、故障诊断等领域的研究都引入了谓词Petri网。
(四)随机Petri网
通过引入时间,在每个变迁的可实施与实施之间联系一个延迟时间,该延迟时间为随机产生的,随机Petri网可广泛应用于过程具有随机特征的系统,取得良好的仿真效果。
(五)模糊Petri网
在基本的Petri网上进行扩展,模糊Petri网的每个库所被赋予一个标识值,该标识值取[0,1]上的实数值,每个变迁获得一个确定因子,规定输入输出函数。模糊Petri网贴近人类的思维认知方式,可用于描述物理系统和社会系统。
四、Petri网的应用
(一)UML形式化
作为一种定义良好、表达方便、面向对象的建模语言,UML已经融入到软件工程中,从需求开发到项目开发、后期维护等全软件生命周期都可以运用UML的思想、方法和技术。UML已经垄断面向对象建模技术的市场,成为可视化建模的行业标准。目前,UML广泛应用于实时系统、指挥控制系统、WEB系统建设、分布式系统等应用领域。
然而,由于缺少严格的形式化语义,UML只能静态建模,不能动态仿真。UML描述的系统模型,缺乏严谨的数学验证和分析,难以在模型中实现仿真,以进行修正,并做进一步的改进。
将半形式化的UML形式化,辅以精确的数学语义定义,对软件系统的需求分析、设计、实现等进行严格的描述、分析和验证,成为当前国内外学者的研究热点。目前,UML形式化的方法主要有两种:直接为UML模型定义形式化的语义、建立非形式化的图形表示和形式化语义之间的映射。通过Petri网技术,可以实现uml模型转换成数学定义严格精确的形式化工具。
把uml中的活动图转化为标记控制的Petri网(LCPN)首先由Bocalatte提出;时间(TPN)技术则通过引入时间因素,将例图、对象图等映射到Petri网,Bondavalli首先提出该思想方法;Saldhana则将面向对象的思想引入Petri网中,建立对象Petri网(OPN),并建立uml模型到OPN的映射,利用Petri网的数学基础对UML模型结果进行分析和验证。
(二)与制造行业结合
通常情况下,加工、物流、信息流三个子系统组成了一个完整的柔性制造系统(Flexible Manufacture System,FMS),可实现物料流和信息流的自动化。FMS系统可以高效、高质量通过多种路径以中小批量加工多种产品。FMS系统需要保证装置设备、物料协调工作,快速响应系统内外部变化,对系统进行及时有效的调整。基础数据、控制数据、状态数据组成了FMS系统的数据体系。
Petri网技术可用于研究离散事件动态系统。FMS系统关注事件的发生与结束,整个系统的活动由事件支持,是典型的离散事件驱动系统。Petri网促进了FMS制造业建模和仿真的研究发展。
基于Petri网的FMS建模和分析方法首先由Narahari和Viswanadham提出。Beck和Krogh则通过对Petri网进行修正,实现了由两个机器人组成的装配系统的仿真建模,并基于Petri网对系统做了仿真模拟,获得了显著的效果。在大型复杂系统的建模方面,需要解决复杂性和模型体积等难题,Borusan创造了基于着色Petri网,提出FMS递进结构的建模方法,为FMS制造系统建模创造了另外一种可能。
由于出色的图形表述能力和缜密的数学定义,Petri网在描述制造业系统的运行过程时可以通过数学分析和图形形象地描述。Petri网技术在FMS制造系统建模有着广阔的应用前景。
(三)应用于工程项目群管理
目前,我国的工程项目管理在管理层次、技术方法、平台建设上相对滞后。工程项目群的管理缺乏层次清晰的整体性控制方案,项目群管理计划、控制技术方法趋于粗放,信息沟通不畅。通过对工程项目群实施过程中的工作流程的抽象化,并定义为计算机可识别的形式化表示,进而选择合适的建模工具实现建模要求,克服传统建模方式的局限。
工程项目构成典型的离散事件动态系统,施工条件复杂,内外部干扰因素多,任务间关系错综复杂,开始时间、执行时间随机变化,具有随机排队等待、事件驱动等特性。Petri网很好地满足了以上所有要求。
Wakefield通过Petri网对两个工程项目进行了建模仿真,开创了Petri网在工程仿真的大门;Sawhney在Wakefield的基础上论证了Petri网对施工计划的动态仿真能力,并阐述了建模的步骤;更多的学者通过引入时间、随机性对工程项目群建模的Petri网进行完善,形成了更加切合现实的建模工具。
(四)其他领域
起源与计算机科学系统研究的Petri网建模技术,首先在计算机科学领域广泛应用,包括分布式系统、资源配置、实时系统等,衍生到计算机的其他领域,比如uml建模形式化、软件工程、网络等。国内外学者先后研究龙Petri网应用于公交系统、制造业系统、工程项目建设、电力系统等,获得了很好的效果,对促进相关领域的理论发展和实际建设起到了很大的作用。
五、Petri网的发展趋势
可以预见,Petri网将往纵向和横向两个方向发展。一方面,由于其独特的特性,完善的数学体系支撑、可视化的图形建模工具使得Petri网可应用于不同的领域,Petri网可完美地融入计算机科学领域的建模、生产制造业的建模仿真等,并对推进相关领域的发展起到重要的作用。另一方面,与不同领域的融合,使得不同的使用条件加入,Petri网需要适应不同的应用场景,必须做出相应的改变,着色Petri网、谓词Petri网、模糊Petri网、赋时Petri网、随机Petri网等高级Petri网技术正是为适应不同应用场景而提出的,更多的高级Petri网技术将会随着应用的需要而创造出来。
参考文献
[1]HU H,LI Z,AL-AHMARI A.Reversed fuzy Petri nets and their application for fault diagnosis[J].Computers&Industrial Enginering,2011,60(4):505-510
[2]杨武,李晓渝,曹泽瀚.一种面向对象Petri网模型的语义和行为分析[J].计算机科学,2005,32(10):220-221.
[3]MADIMAN M,TETALI P.Sandwich bounds for joint entropy[C].IEEE International Symposiumon Information Theory,June24-29,2007,Nice,France:511-515.
[4]李再华,白晓民,周子冠.基于特征挖掘的电网故障诊断方法[J].中国电机工程学报,2010,30(10):16-22.
智能Petri网研究进展 第6篇
Petri网是一种可以用网状图形表示的系统模型, 它把尊重自然规律作为第一要义, 用图形化的语言描述系统的运行特征, 适于表达和描述离散事件动态系统的动态变化和静态结构[1]。Petri网最常用的是图形化表示方法, 在一些复杂系统中状态和变迁比较多时, Petri网就会存在状态空间爆炸等问题, 因此Petri网的简化以及与其他技术相结合成为进一步研究的重点。经过将近50年的发展Petri网的纵向发展取得显著成果, Petri网理论的发展趋于完善;横向发展表现为从基本的条件/时间网, 发展到高级网, 与其他领域的技术如面向对象技术[2]、计算智能技术的结合, 使得Petri网更适用于生产实践中。
计算智能又称为智能计算、软计算, 以生物进化的观点认识和模拟智能, 通常被认为是人工智能的一个方面[3], 其通过借用自然界生物界规律的启迪, 根据其原理模仿设计求解问题。计算智能的主要方法包括模糊逻辑、人工神经网络、遗传算法、蚁群算法、粗糙集、进化算法、免疫算法等。本文主要介绍Petri网与模糊逻辑、遗传算法、蚁群算法、粗糙集、神经网络这五种方法的结合方式及主要应用。
2 模糊Petri网
模糊理论的基本思想可以概括为:认为模糊性现象是存在的, 以处理概念模糊不确定的事物为其研究目标, 并积极地将其严密地量化成计算机可以处理的信息, 不主张用繁杂的数学分析即模型来解决模型[4]。模糊技术与Petri网结合产生了模糊Petri网 (Fuzzy Petri Net, FPN) [5], 它是对普通Petri网的模糊化。与普通Petri网相比, FPN具有独有的特点:首先, FPN的每一个库所被赋予了一个置信度, 用[0, 1]之间的一个实数来表示;其次, 对于每一个变迁赋予一个变迁因子来表示其发生的概率;第三, 规定了输入输出函数。FPN形式的用七元组表示, 包括库所、变迁、确信度、阈值和权值五部分。模糊Petri网的产生式规则往往包含类似与、或的连接符, 将简单规则、组合规则以及对应的FPN相结合产生对应的模型[6,7,8,9]。
目前研究人员对模糊Petri网建模有了一定的研究。文献[6-10]对FPN在故障诊断中的应用进行了一系列的研究, 发现Petri网尤其在电网故障诊断方面取得较好效果。模糊Petri网及其改进算法在故障诊断研究方面逐渐受到青睐。文献[6]在模糊Petri网的基础上引入了人工神经网络技术, 给出了神经网络与模糊Petri网结合的表示方法并根据工程机械故障诊断的特点提出了故障诊断的模糊神经Petri网模型, 使得FPN具有很强的推理适应能力和自适应性, 文献[11]探讨了四种优化算法:遗传、BP、蚁群、克隆选择, 在模糊Petri网参数寻优中的应用, 提高了模糊Petri忘得泛化能力和自适应能力。文献[12]提出一种改进的基于方向性加权的FPN模型, 应用于电网故障诊断中减少了计算量, 能够用在信息不完备的情况中给出正确的诊断结果。随着FPN在故障诊断中应用的不断研究, 有研究人员将FPN与故障Petri网结合起来提出模糊故障Petri网模型[13], 既模拟了故障传播的过程, 同时又可以进行模糊推理, 提高了实用性。此外还对FPN的知识和模糊推理方法进行了研究[14,15,16]。
FPN是目前研究与应用最为广泛的一种Petri网, 因为它更加符合人类的思维和认知方式, 体现出Petri网表达同步并发事件的能力, 而且将结果以概率的形式给出使人能够更直观地进行结果认知。
3 遗传Petri网
遗传算法是进化计算的一种, 是借鉴生物自然遗传的基本原理用于自然和人工系统的自适应行为研究和串编码技术。遗传算法的基本操作有选择、交叉和变异。可以不依赖问题本身的方式对未知空间进行有效搜索找出问题的解[17]。
遗传算法与Petri网的结合可以归为以下几类。
3.1 遗传算法嵌入Petri网
首先利用Petri网对整个系统进行建模, 然后遗传算法用来对Petri网中的参数进行优化或者对整个模型进行调度并取得最优解[18,19,20,21,22]。文献[18]中利用Petri网对柔性制造系统进行建模, 然后对Petri网中的元素利用遗传算法求得最优解, 有较高的通用性。文献[19]首先运用一种高级Petri网赋时库所Petri网对所研究的问题进行建模, 然后利用遗传算法对建立的Petri网模型进行最优值求解。文献[20]将遗传算法引入到模糊Petri网的参数寻优过程之中, 使得模糊Petri网的建立能够不依赖实际经验, 对初始数据的依赖性降低提高了模糊Petri网的泛化能力和学习能力。文献[21]以Petri网对系统进行建模, 然后将遗传算法作为调度策略嵌入到建立的模型之中, 实现了在正确调度的基础上对生产过程的有效描述。
此种结合方法能够很好地利用Petri网与遗传算法各自优点, 一般用于计划优化、调度优化等优化问题中。
3.2 利用Petri网对遗传算法进行性能分析
首先利用Petri网建立遗传算法的模型, 通过所建立的模型对遗传算法进行性能分析, 计算得出遗传算法各个步骤的利用率和性能指标, 为遗传算法的改进提供可靠依据[23]。为遗传算法的可靠性检验提供了一种新思路。
Petri网与遗传算法相结合, 要解决的问题首先是Petri网的应用问题, 如模型的可重用性、复杂度和可维护性等问题。其次要解决遗传算法与Petri网的结合方式, 根据不同的应用背景选择不同的嵌入方式。
4 蚁群Petri网
蚁群算法是群集智能的典型算法, 是一种新型的模拟进化算法, 它模拟蚁群的觅食行为, 利用信息素的反馈机制来求得最佳路径即全局最优解, 具有分布式计算、正反馈和贪婪地启发式搜索等主要特点[24]。能够很好地解决组合优化问题, 蚁群算法的主要应用方向为路径优化和物流配送。Petri网与蚁群算法相结合能充分利用Petri网表达系统直观精细和蚁群算法快速收敛的特点。
目前研究者对Petri网与蚁群算法结合进行了一系列的研究。Petri网与蚁群算法结合也是双向的, 一方面可以用来改进蚁群算法, 另一方面可以用来改进Petri网建模。文献[25]将蚁群算法与广义Petri网结合, 提高了蚁群算法的搜索速度, 而且优化算法的搜索结果。文献[26]用蚁群觅食行为引起的最短滤镜来减少Petri网的状态爆炸问题。黄光球[27]等人提出一种可以记录少量信息的记忆时间Petri网, 使托肯类比为蚂蚁, 托肯在网中行走并留下信息素从而得到Petri网中最短的变迁序列;石立宝[28]等人提出一种蚁群条件禁忌混合计算智能算法来求解Petri网的路径寻优问题, 快速得到Petri网的最短时延路径。蚁群算法还进一步应用在模糊Petri网的参数寻优问题中, 其中李洋等把蚁群算法中的最大-最小系统引入到模糊Petri网的参数寻优过程提出一种基于线程实现技术的参数优化算法, 使模糊Petri网具有较强的泛化能力和自适应功能[29];周恺卿、肖增良等人研究了蚁群算法跟智能方法结合并运用到模糊Petri网的参数寻优中, 不依赖于经验数据对初始输入无要求[30,31]。
在应用方面, 对蚁群算法与Petri网结合的路径优化问题的在具体应用上进行了研究。其中朱伟等引入一种具有“动态托肯”和“静态托肯”的扩展Petri网对物流配送进行建模并使用改进了的蚁群算法对其进行最优路径求解, 缩短了求解时间[32]。将蚁群算法与Petri网结合还可以应用在解决柔性装配系统的调度问题上[33,34,35,36], 最后确定装配系统的时延Petri网模型。
蚁群算法与Petri网的结合能够很好地解决Petri网路径寻优和模糊Petri网的参数优化问题, 为模糊Petri网的参数优化提供一种新方法。
5 粗糙Petri网
粗糙集 (RST) 是一种可以实现知识提取的很好的数学工具, 自被提出以来[37], 成功地解决数据约简、知识提取、数据重要性评估、决策规则提取、数据推理解释等问题[38]。粗糙集与Petri网结合能够充分利用粗糙的属性约简这一功能, 降低Petri网建模的复杂性。
目前研究人员对粗糙集在Petri网中的应用进行了研究。粗糙集与Petri网技术结合主要是利用粗糙集对专家系统的知识进行约简从而获得最小有效规则, 然后建立Petri网模型, 从而避免了Petri网出现组合爆炸的问题, 实现对Petri网模型的简化[39]。目前这种结合方式在故障诊断中的应用成为研究的热点[40,41,42,43,44,45]。文献[40]中将此方法运用到直线感应电机参数优化诊断中, 提出利用粗糙集的关联规则挖掘算法将含有冗余信息的复杂的系统进行简化并证明了正确性与有效性;文献[41]将此种方法运用于旋转机械故障诊断中并证明了方法的有效性。文献[42]提出在电力变压器的故障诊断中利用粗糙集信息表简化技术实现专家知识的简化与故障特征的压缩, 得到最小诊断规则, 然后利用Petri网对最小诊断规则进行建模与模糊推理, 实现了诊断的高效性、计算的快速准确性, 而且更易于理解。文献[43]利用粗糙集知识约简和处理不确定信息的能力对变电站的故障诊断知识实现属性优选, 然后运用Petri网对最小诊断规则建模推理。文献[44]将此种结合方法运用到断路器故障诊断中, 利用粗糙集的规则提取矩阵算法和区分矩阵算法对决策表实现条件属性约简再建立Petri网模型。兰华等人将粗糙集结合Petri网运用到分区域并行推理的配电网故障诊断中, 实现了诊断的快速准确并且有良好的容错能力和适应性[45]。
6 神经网络Petri网
20世纪80年代以来掀起了对人工神经网络研究的热潮[3], 人工神经网络以其较强的自学习、自适应和自组织能力, 非常适合于分布式、大规模并行信息的存储和处理。神经网络运用到Petri网中可以提高Petri网的自学习能力和自适应能力, 使Petri应用范围进一步扩大。
目前研究人员主要研究的是人工神经网络与模糊Petri网的结合, 主要有两方面结合方式。一是将人工神经网络用于模糊Petri网的参数优化和权值寻优之中[6,11,46]。模糊Petri网是一种应用比较广泛的Petri网, 但是模糊Petri网权值、阈值和确信度参数的确定一直是根据专家经验产生的, 有些经常是难以确定的。神经网络以其自适应能力和自学习能力, 经过样本数据训练可以获得权值、阈值和确信度参数的参考值或者比较准确的参数。文献[47]将BP神经网络的反向传递算法引入到模糊Petri网参数寻优中, 并证明方法的有效性。文献[48]将神经网络优化权值的FPN用于雷达的故障诊断, 与传统诊断方法相比具有许多优势。二是将人工神经网络融合到Petri网中建立一种模糊神经Petri网模型[6], 用于故障诊断中故障原因和故障现象之间关系无法确定的情况。
7 结束语
Petri网作为一种良好的建模工具, 其与计算智能方法的结合不仅优化了Petri网模型, 使Petri网建模更加容易, 而且提高了Petri网的自适应性与自学习能力, 使其应用范围进一步扩大。
有色Petri网论文 第7篇
云计算将计算任务分布在大量计算机构成的资源池上,是一种商业计算模型。它使用户能够按需获取计算能力、存储空间和信息服务[1,2]。由于云计算是多种技术共同演进的结果,又有大公司推动,其成熟度较高,发展极为迅速。Google、亚马逊、IBM、微软和Yahoo等大公司都是云计算的先行者,其中Google是最大的云计算技术的使用者。
Google的诀窍在于它发展出简单而又高效的技术,让百万台以上廉价计算机协同工作,共同完成一些前所未有的任务,这些技术被命名为Google云计算技术。其中,MapReduce[3]使得海量信息的并行处理变得简单易行。MapReduce是Google提出的一个软件架构,是一种处理海量数据的并行编程模式,用于大规模数据集的并行计算。
本文在研究MapReduce逻辑模型的基础上,为其建立了随机Petri网模型。其模型符合随机Petri网工作流系统的性质,因此利用随机Petri网的工作流系统的性能等价公式,对该模型的性能进行分析,并最终求出整个系统的性能参数。
1 Petri网的相关知识
1.1 随机Petri网概述
定义1(随机Petri网[4,5]) 连续时间SPN=(P,T;F,W,M0,λ),其中(P,T;F,W,M0)是一个P/T系统,λ=(λ1,λ2,…,λm)是变迁平均实施速率集合。λi是变迁的平均实施速率,表示在可实施情况下单位时间内的平均实施次数,单位是次数/单位时间。
平均实施速率的倒数τi=1/λi称为变迁τi的平均实施延时或平均服务时间。每个λi的值是从对所模拟系统的实际测量中获得的或根据某种要求的预测值,因此这些值具有实际的物理意义。
1.2 工作流的性能评价
在通常情况下,假设工作流模型的变迁延时是服从指数分布函数的,因为这种假定本身是与现实中多数系统相符合的。在实际系统中,大多数情况下服务器的服务时间是接近指数分布的。工作流主要由四种基本模型组成:串联模型,并联模型,选择模型,循环模型。文献[4,5]已基于Petri网状态方程对这四种工作流基本模型的性能等价公式进行了详细的推导。本文将在对MapReduce的随机Petri网模型的研究分析中引用相关结论。
2 MapReduce的逻辑模型
MapReduce把运行在大规模集群上的并行计算过程抽象为两个函数:Map和Reduce,即映射和化简[1,2,3]。简单说,MapReduce就是“任务的分解和结果的汇总”。Map把任务分解成为多个任务,Reduce把分解后多任务处理的结果汇总起来得到最终结果。一个MapReduce操作分为两个阶段:映射阶段和化简阶段。用MapReduce处理大数据集的过程如图1所示。
3 MapReduce的随机Petri网建模
在此将具体分析MapReduce操作两个阶段完成的工作,并建立随机Petri网模型。在映射阶段,MapReduce框架将用户输入的数据分割为M个片段,对应M个Map任务。每一个Map操作的输入是数据片段中的键值对<K1,V1>集合,该过程在随机Petri网模型中用瞬时变迁tstart(i)表示;Map操作调用用户定义的Map函数,输出一个中间态的键值对<K2,V2>集合。接着,按照中间态的K2将输出的数据集进行排序,并生成一个新的<K2,list(V2)>元组,这样可以使得对应同一个键的所有值的数据都在一起。然后,按照K2的范围将这些元组分割为R个片段,对应Reduce任务的数目,该过程在随机Petri网模型中用变迁tij表示。在化简阶段,每一个Reduce操作的输入是一个<K2,list(V2)>片段,Reduce操作调用用户定义的Reduce函数,生成用户需要的键值对<K3,list(V3)>进行输出,该过程在随机Petri网模型中用瞬时变迁tend(j)表示。其中:0≤i≤m-1;0≤j≤n-1。通过上述分析,给出相应Petri网模型,如图2所示。
4 随机Petri网模型的工作流系统的性能分析
下面对上节中给出的MapReduce的随机Petri网模型,利用文献[4,5]中的工作流的各种随机Petri网模型的性能等价公式进行性能分析。
4.1 变迁延迟时间的假定
为了说明MapReduce模型的性能,根据各个环节实际中可能的执行速率,将随机Petri网模型中变迁的平均实施速率取定一些随机值。现假设变迁tij平均延迟时间(单位为分钟)为1/λij。在tij处均有分支选择,假定执行变迁tij的概率为aij。下面计算该过程性能等价时间。
4.2 性能等价计算
第1步:根据输入端的形态以及选择模型[4,5]的性能等价公式计算由变迁tij,其中,0≤i≤m-1;0≤j≤n-1组成的选择模型的性能等价时间:
第2步:对输入端进行处理之后,输出端的结构符合工作流的并联随机Petri网模型,根据并联模型[4,5]的性能等价计算公式,性能等价时间为:
式中λi的取值情况参照式(1)。
经过层层分析,最终求出整个系统的性能等价时间,继而可求出其他的性能参数,如吞吐率、系统中平均作业数等。
5 结 语
本文首先描述了MapReduce的逻辑模型,并为其建立了随机Petri网模型。本文所建立的随机Petri网模型符合随机Petri网工作流系统的性质,因此利用随机Petri网的工作流系统的性能等价公式,对模型的性能进行了分析。在随机Petri网模型的性能分析中,利用给出的性能等价公式,不断地进行性能等价化简,最终求出整个系统的性能参数。
摘要：首次提出用随机Petri网为MapReduce逻辑模型建立Petri网模型的思想,目的在于采用随机Petri网工作流性质对其进行分析。因此,在研究MapReduce逻辑模型的基础上,为其建立了随机Petri网模型。该随机Petri网模型符合随机Petri网工作流系统的性质,本文利用随机Petri网的工作流系统的性能等价公式,分析了模型的性能,最终求出整个系统的性能参数。该性能参数能够很好地说明MapReduce处理大数据集的优势。
关键词：云计算,MapReduce,随机Petri网,建模,性能分析
参考文献
[1]刘鹏.云计算[M].2版.北京:电子工业出版社,2011.
[2]ARMBRUST Michael,FOX Armando,GRIFFITH Rean,et al.Above the clouds:a berkeley view of cloud computing[R].US:UC Berkeley RAD Laboratory,2009.
[3]DEAN Jeffrey,GHEMAWANT Sanjay.Simpled data pro-cessing on large clusters[J/OL].[2009-07-13].http://www.blog.csdn.net.
[4]蒋昌俊.离散事件动态系统的PN机理论[M].北京:科学出版社,2000.
[5]林闯,曲扬,郑波,等.一种随机Petri网性能等价化简与分析方法[J].电子学报,2002,30(11):1620-1623.
【有色Petri网论文】相关文章：
有色金属论文提纲08-19
有色采矿工程论文05-05
有色金属论文范文05-10
有色采矿工程论文提纲10-07
有色冶金安全工程科技论文04-20
有色冶金专业毕业论文题目04-04
有色金属工业发展论文05-04
内部控制有色冶金企业风险论文04-11
有色金属工业发展论文提纲09-12
勘查有色金属矿产资源论文04-16