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 generalized stochastic Petri nets,CGSPN)的复杂...因大量采用分布式、综合化、模块化方案,复杂电子系统极易出现共因故障和故障并发等新问题,传统测试性参数确定方法难以解决。针对这一问题,提出一种基于着色广义随机Petri网(colored generalized stochastic Petri nets,CGSPN)的复杂电子系统测试性参数确定新方法。首先,综合需求信息、约束边界和维修保障等要求,建立电子系统两层级CGSPN模型,引入着色,实现不同模块各种状态的实时追踪和故障并发处理,通过广义随机处理共因故障的随机不确定性;然后,利用着色和可用度探索一种带有冗余设计的测试性参数处理手段,丰富测试性体系;最后,构建一种不同模块、各种状态融合的并行分析技术,统一系统层和模块层之间的状态转移关系,避免分阶段串行处理和等效替换。以通信导航识别系统为例进行实例分析,所提方法比传统方法具有更好的可用性和有效性。展开更多
铁路信号安全协议-Ⅱ(railway signal safety protocol-Ⅱ,RSSP-Ⅱ)是我国列车控制系统CTCS-3的核心安全通信协议,在保障列车通信安全性与可靠性方面发挥着关键作用。然而,现有研究表明,RSSP-Ⅱ的消息鉴定安全层存在密钥恢复与伪造等安...铁路信号安全协议-Ⅱ(railway signal safety protocol-Ⅱ,RSSP-Ⅱ)是我国列车控制系统CTCS-3的核心安全通信协议,在保障列车通信安全性与可靠性方面发挥着关键作用。然而,现有研究表明,RSSP-Ⅱ的消息鉴定安全层存在密钥恢复与伪造等安全漏洞,可能危及列车控制系统的稳定运行。针对上述安全问题,使用着色Petri网(colored Petri nets,CPN)形式化建模方法对RSSP-Ⅱ进行了分析,验证了RSSP-Ⅱ中存在安全漏洞,并提出了一种改进协议EN-RSSP(enhanced railway signal safety protocol)。该改进协议主要包含3个方面的增强措施。首先,通过可信第三方在安全信道中动态构建通信双方设备的临时密钥对;其次,基于椭圆曲线双线性对的离散对数困难特性,结合哈希函数实现会话密钥协商;最后,采用由会话密钥和通信双方设备的预共享密钥构成的双密钥加密体系对消息进行加密传输。此外,还在信息交互过程中引入了时间戳和CMAC(cipher-based message authentication code)消息认证码,以确保通信双方消息的保密性和完整性。通过CPN形式化分析工具对EN-RSSP(enhance-RSSP)和RSSP-Ⅱ进行安全评估,结果表明,改进后的协议不仅能有效抵御密钥恢复与伪造攻击,还可防范重放攻击,显著提升了系统的安全性。展开更多
本文采用的着色Petri网(Colored Petri Nets,CPN)是一种基于模型检测法的自动化建模技术,它引入了"颜色集"的概念,以扩展Petri网的表达能力。该技术利用着色Petri网及其配套的建模工具CPN Tools对安全协议进行建模,能够使得...本文采用的着色Petri网(Colored Petri Nets,CPN)是一种基于模型检测法的自动化建模技术,它引入了"颜色集"的概念,以扩展Petri网的表达能力。该技术利用着色Petri网及其配套的建模工具CPN Tools对安全协议进行建模,能够使得模型实现图形化和层次化,其内置的状态空间分析工具及CPN ML语言,能够高效地协助分析人员获取必要数据。本文以经典的密钥交换协议TMN为例,运用CPN方法对其进行形式化分析,成功识别出攻击者可能利用的攻击路径,并验证了协议中存在的安全漏洞。针对这些漏洞,本文提出了一种改进方法,经过验证,证实了该改进方法的有效性。展开更多
基金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 generalized stochastic Petri nets,CGSPN)的复杂电子系统测试性参数确定新方法。首先,综合需求信息、约束边界和维修保障等要求,建立电子系统两层级CGSPN模型,引入着色,实现不同模块各种状态的实时追踪和故障并发处理,通过广义随机处理共因故障的随机不确定性;然后,利用着色和可用度探索一种带有冗余设计的测试性参数处理手段,丰富测试性体系;最后,构建一种不同模块、各种状态融合的并行分析技术,统一系统层和模块层之间的状态转移关系,避免分阶段串行处理和等效替换。以通信导航识别系统为例进行实例分析,所提方法比传统方法具有更好的可用性和有效性。
文摘铁路信号安全协议-Ⅱ(railway signal safety protocol-Ⅱ,RSSP-Ⅱ)是我国列车控制系统CTCS-3的核心安全通信协议,在保障列车通信安全性与可靠性方面发挥着关键作用。然而,现有研究表明,RSSP-Ⅱ的消息鉴定安全层存在密钥恢复与伪造等安全漏洞,可能危及列车控制系统的稳定运行。针对上述安全问题,使用着色Petri网(colored Petri nets,CPN)形式化建模方法对RSSP-Ⅱ进行了分析,验证了RSSP-Ⅱ中存在安全漏洞,并提出了一种改进协议EN-RSSP(enhanced railway signal safety protocol)。该改进协议主要包含3个方面的增强措施。首先,通过可信第三方在安全信道中动态构建通信双方设备的临时密钥对;其次,基于椭圆曲线双线性对的离散对数困难特性,结合哈希函数实现会话密钥协商;最后,采用由会话密钥和通信双方设备的预共享密钥构成的双密钥加密体系对消息进行加密传输。此外,还在信息交互过程中引入了时间戳和CMAC(cipher-based message authentication code)消息认证码,以确保通信双方消息的保密性和完整性。通过CPN形式化分析工具对EN-RSSP(enhance-RSSP)和RSSP-Ⅱ进行安全评估,结果表明,改进后的协议不仅能有效抵御密钥恢复与伪造攻击,还可防范重放攻击,显著提升了系统的安全性。
文摘本文采用的着色Petri网(Colored Petri Nets,CPN)是一种基于模型检测法的自动化建模技术,它引入了"颜色集"的概念,以扩展Petri网的表达能力。该技术利用着色Petri网及其配套的建模工具CPN Tools对安全协议进行建模,能够使得模型实现图形化和层次化,其内置的状态空间分析工具及CPN ML语言,能够高效地协助分析人员获取必要数据。本文以经典的密钥交换协议TMN为例,运用CPN方法对其进行形式化分析,成功识别出攻击者可能利用的攻击路径,并验证了协议中存在的安全漏洞。针对这些漏洞,本文提出了一种改进方法,经过验证,证实了该改进方法的有效性。
