基于HCPN模型的TLS1.3协议安全性分析

传输层(Transport Layer Security,TLS)协议是保证网络传输安全的重要标准协议,实现了数据加密和数据完整性以及身份验证。由于TLS协议一直存在很多安全漏洞,因此不断更新。目前最新版本TLS1.3(RFC 8846)已经发布,较之前TLS1.2(RFC 5246)在协议内容上有很大改进,提高了安全性和传输效率。使用层次着色Petri网(HCPN)的建模方法对TLS1.3握手协议进行建模,同时添加Delov-Yao攻击模型,并分析了对应模型下的状态空间报告。实验结果表明新发布的TLS1.3握手协议预主密钥有良好的机密性,并且身份认证满足协议规范的安全属性要求。目前国内在协议形式化分析方法的研究方面很少,本文研究在协议形式化分析方法上对其他协议分析具有理论指导意义。

煤矿辅助运输调度系统的层次颜色Petri网建模

为实现煤矿井下无轨运输车辆的安全调度,提出一种新型调度策略,以此为框架,利用层次颜色Petri网对调度系统进行建模。通过研究模型的运行过程,对调度策略的安全性、正确性及可重用性进行证明。同时,利用模型的状态空间报告对调度系统基本性能作简单分析。结果表明,该调度系统模型可对车辆运输量、区段使用频度及其时间分布以及车辆运输速度与运输任务产生速度的匹配程度进行分析,在应用过程中可以有效提高车辆运输安全性,避免运输事故,辅助管理者规划运输任务,提高矿井辅助运输效率。

基于着色Petri网的HDFS数据一致性建模与分析

HDFS分布式文件系统作为Apache Hadoop的核心组件之一,在工业界得到了广泛应用.HDFS采用了多副本机制保证数据的可靠性,但是由于多副本的存在,在节点失效、网络中断、写入失败时可能会导致数据不一致.与传统文件系统相比,HDFS被认为其数据一致性有所降低,但用户并不知道何时会出现不一致的情况,目前也没有相关工作对其一致性机制进行验证说明.当数据存在一致性问题时,会增加上层应用的不确定性.可见,对数据一致性的研究十分必要.HDFS的软件规模庞大,且在分布式环境下运行,针对这些特点,采用了着色Petri网建模和状态空间分析的方法,完成了以下工作:(1)使用着色Petri网对HDFS的读写流程建立模型,该模型详细刻画了HDFS内部各个组件的功能及相互协作的机制;(2)基于着色Petri网模型,使用状态空间工具分析了HDFS的数据层一致性和操作层一致性,验证并详细说明了HDFS出现不一致的条件;(3)在分析过程中,提出了“时点重复读”的操作层一致性验证方法,采用串行化的重复读策略降低了状态空间复杂度.基于以上工作,针对HDFS上层应用的开发给出建议,帮助提高应用的数据一致性.此外,在建模过程中提出的建模技巧给基于CPN Tools工具分析其他系统提供了借鉴.

基于Petri网军民共用停机坪运行仿真与分析

为解决军民用停机坪运行冲突问题,通过分析军用飞机与民用飞机共同使用机坪及其附近区域的滑行规则,基于模块化建模思想,建立基于停机坪区域的分层赋时着色Petri网模型。提出冲突点选择避让机制,设计运行模型控制器,将场面运行控制知识与模块的库所和变迁集成,增强模型的智能决策能力,基于CPN Tools软件平台实现模块化建模。结果表明,采用规则的算法模型能有效减少军用飞机与民用飞机冲突,实现冲突解脱控制,验证了模型的有效性,保证军民用飞机高效、有序运行。

基于层次着色Petri网的物资储配系统调度问题研究

采用层次着色Petri网研究了物资储配系统的调度问题。用首层Petri网给出了系统运行过程的总体宏观描述,在层次Petri网子页中对固定货架子系统、旋转货架子系统、分拣子系统和输送子系统的动态行为进行了详细刻画。在CPN-Tools仿真环境中分析了系统的整体动态特性,给出并验证了系统的总体调度策略。

基于Petri网与多代理的半导体调度系统建模及仿真

为解决半导体生产系统作业调度问题,提出了一种基于层次赋时着色Petri网(HTCPN)与多代理系统(MAS)的调度系统建模与仿真方法。以半导体“图案成型”生产系统为对象,分析该系统调度问题的约束条件和多目标函数,设计MAS的组织结构和基于招标-投标策略的调度机制,结合HTCPN建模方法建立调度系统模型,最后采用仿真软件CPN Tools验证了该调度系统的可行性和有效性。

Verification of Session Initiation Protocol Using Timed Colored Petri Net

In this work, Session Initiation Protocol model is established by using Timed Colored Petri Nets (TCPN). SIP (Session Initiation Protocol) is a protocol developed to assist in providing advanced telephony services across the Internet. The Session Initiation Protocol (SIP) has become the quasi-standard for Voiceover-Internet Protocol (VoIP) communications. SIP is based on a client–server infrastructure in which user agents represent the end-terminals as clients, proxy servers handle SIP message routing between the user agents, and registrar servers store the client’s contact information into a location service. By use of timed color set and useful time attributes in tokens defined in CPN tools, timer and time-related problems of SIP are modeled and analyzed. Timer is an important part for SIP, especially the INVITE transaction.

有色Petri网在web服务组合建模中的应用

以分布、异构、多自治域的互联网环境为背景,提出利用有色Petri网对web服务组合进行建模的方法,给出了web服务组合网的形式化描述和常用结构的图形化表示方法。文中所引用的案例模型可以在CPN-tools中测试,有效的建模是模型分析验证和模型应用的基础。对电子商务和企业应用集成在解决web服务组合问题中具有一定的参考价值。