针对航班地面保障实际作业流程的精准刻画与性能评估,提出一种多层级航班地面保障随机Petri网(Stochastic Petri Net,SPN)构建及性能分析方法.将保障节点间的衔接过程与保障节点进行过程同时作为随机Petri网的变迁,构建多层级航班地面保...针对航班地面保障实际作业流程的精准刻画与性能评估,提出一种多层级航班地面保障随机Petri网(Stochastic Petri Net,SPN)构建及性能分析方法.将保障节点间的衔接过程与保障节点进行过程同时作为随机Petri网的变迁,构建多层级航班地面保障SPN模型解析保障全流程复杂的串并联关系.采用时间性能等价化简方法降低模型分析的难度,在此基础上建立同构马尔科夫链对模型进行性能分析,得到多层级航班地面保障流程SPN模型的库所繁忙率和变迁利用率.建立的输入输出库所繁忙率四象限图可直观揭示流程中的低效与高效运行区域,实现保障节点及衔接过程前后续状态的精准分类,结合变迁利用率结果,并基于变迁平均发生速率动态变化过程中稳态概率累计变化量识别关键保障节点或衔接,包括4个关键保障节点及6个关键节点间的衔接.研究结果表明:航班地面保障的关键部分多集中在前后衔接不紧密的不同节点间,如餐食及机供品配供完成后等待关客舱门衔接过程,即使单个保障节点的作业时间较短,但若其前续准备或后续完成状态耗时较长,易导致整体保障效率降低;当关键保障节点或衔接平均发生速率超过0.2,即对应持续时间缩短至5 min后,保障流程整体持续时间下降趋于稳定.研究成果可以为机场协同决策下目标撤轮挡时间预测准确性的提高及促进机坪运行保障效率提供理论基础和方法支撑.展开更多
A novel siphon-based divide-and-conquer(SbDaC)policy is presented in this paper for the synthesis of Petri net(PN)based liveness-enforcing supervisors(LES)for flexible manufacturing systems(FMS)prone to deadlocks or l...A novel siphon-based divide-and-conquer(SbDaC)policy is presented in this paper for the synthesis of Petri net(PN)based liveness-enforcing supervisors(LES)for flexible manufacturing systems(FMS)prone to deadlocks or livelocks.The proposed method takes an uncontrolled and bounded PN model(UPNM)of the FMS.Firstly,the reduced PNM(RPNM)is obtained from the UPNM by using PN reduction rules to reduce the computation burden.Then,the set of strict minimal siphons(SMSs)of the RPNM is computed.Next,the complementary set of SMSs is computed from the set of SMSs.By the union of these two sets,the superset of SMSs is computed.Finally,the set of subnets of the RPNM is obtained by applying the PN reduction rules to the superset of SMSs.All these subnets suffer from deadlocks.These subnets are then ordered from the smallest one to the largest one based on a criterion.To enforce liveness on these subnets,a set of control places(CPs)is computed starting from the smallest subnet to the largest one.Once all subnets are live,this process provides the LES,consisting of a set of CPs to be used for the UPNM.The live controlled PN model(CPNM)is constructed by merging the LES with the UPNM.The SbDaC policy is applicable to all classes of PNs related to FMS prone to deadlocks or livelocks.Several FMS examples are considered from the literature to highlight the applicability of the SbDaC policy.In particular,three examples are utilized to emphasize the importance,applicability and effectiveness of the SbDaC policy to realistic FMS with very large state spaces.展开更多
本文采用的着色Petri网(Colored Petri Nets,CPN)是一种基于模型检测法的自动化建模技术,它引入了"颜色集"的概念,以扩展Petri网的表达能力。该技术利用着色Petri网及其配套的建模工具CPN Tools对安全协议进行建模,能够使得...本文采用的着色Petri网(Colored Petri Nets,CPN)是一种基于模型检测法的自动化建模技术,它引入了"颜色集"的概念,以扩展Petri网的表达能力。该技术利用着色Petri网及其配套的建模工具CPN Tools对安全协议进行建模,能够使得模型实现图形化和层次化,其内置的状态空间分析工具及CPN ML语言,能够高效地协助分析人员获取必要数据。本文以经典的密钥交换协议TMN为例,运用CPN方法对其进行形式化分析,成功识别出攻击者可能利用的攻击路径,并验证了协议中存在的安全漏洞。针对这些漏洞,本文提出了一种改进方法,经过验证,证实了该改进方法的有效性。展开更多
文摘针对航班地面保障实际作业流程的精准刻画与性能评估,提出一种多层级航班地面保障随机Petri网(Stochastic Petri Net,SPN)构建及性能分析方法.将保障节点间的衔接过程与保障节点进行过程同时作为随机Petri网的变迁,构建多层级航班地面保障SPN模型解析保障全流程复杂的串并联关系.采用时间性能等价化简方法降低模型分析的难度,在此基础上建立同构马尔科夫链对模型进行性能分析,得到多层级航班地面保障流程SPN模型的库所繁忙率和变迁利用率.建立的输入输出库所繁忙率四象限图可直观揭示流程中的低效与高效运行区域,实现保障节点及衔接过程前后续状态的精准分类,结合变迁利用率结果,并基于变迁平均发生速率动态变化过程中稳态概率累计变化量识别关键保障节点或衔接,包括4个关键保障节点及6个关键节点间的衔接.研究结果表明:航班地面保障的关键部分多集中在前后衔接不紧密的不同节点间,如餐食及机供品配供完成后等待关客舱门衔接过程,即使单个保障节点的作业时间较短,但若其前续准备或后续完成状态耗时较长,易导致整体保障效率降低;当关键保障节点或衔接平均发生速率超过0.2,即对应持续时间缩短至5 min后,保障流程整体持续时间下降趋于稳定.研究成果可以为机场协同决策下目标撤轮挡时间预测准确性的提高及促进机坪运行保障效率提供理论基础和方法支撑.
基金The authors extend their appreciation to King Saud University,Saudi Arabia for funding this work through the Ongoing Research Funding Program(ORF-2025-704),King Saud University,Riyadh,Saudi Arabia.
文摘A novel siphon-based divide-and-conquer(SbDaC)policy is presented in this paper for the synthesis of Petri net(PN)based liveness-enforcing supervisors(LES)for flexible manufacturing systems(FMS)prone to deadlocks or livelocks.The proposed method takes an uncontrolled and bounded PN model(UPNM)of the FMS.Firstly,the reduced PNM(RPNM)is obtained from the UPNM by using PN reduction rules to reduce the computation burden.Then,the set of strict minimal siphons(SMSs)of the RPNM is computed.Next,the complementary set of SMSs is computed from the set of SMSs.By the union of these two sets,the superset of SMSs is computed.Finally,the set of subnets of the RPNM is obtained by applying the PN reduction rules to the superset of SMSs.All these subnets suffer from deadlocks.These subnets are then ordered from the smallest one to the largest one based on a criterion.To enforce liveness on these subnets,a set of control places(CPs)is computed starting from the smallest subnet to the largest one.Once all subnets are live,this process provides the LES,consisting of a set of CPs to be used for the UPNM.The live controlled PN model(CPNM)is constructed by merging the LES with the UPNM.The SbDaC policy is applicable to all classes of PNs related to FMS prone to deadlocks or livelocks.Several FMS examples are considered from the literature to highlight the applicability of the SbDaC policy.In particular,three examples are utilized to emphasize the importance,applicability and effectiveness of the SbDaC policy to realistic FMS with very large state spaces.
文摘本文采用的着色Petri网(Colored Petri Nets,CPN)是一种基于模型检测法的自动化建模技术,它引入了"颜色集"的概念,以扩展Petri网的表达能力。该技术利用着色Petri网及其配套的建模工具CPN Tools对安全协议进行建模,能够使得模型实现图形化和层次化,其内置的状态空间分析工具及CPN ML语言,能够高效地协助分析人员获取必要数据。本文以经典的密钥交换协议TMN为例,运用CPN方法对其进行形式化分析,成功识别出攻击者可能利用的攻击路径,并验证了协议中存在的安全漏洞。针对这些漏洞,本文提出了一种改进方法,经过验证,证实了该改进方法的有效性。
