基于CPN的智能合约交易顺序依赖漏洞的验证

智能合约的形式化验证工作主要集中在编程语言层面的漏洞研究,而交易顺序依赖作为区块链层面的漏洞更不易被检测。基于着色Petri网对智能合约中潜在的交易顺序依赖漏洞进行形式化验证。以Decode悬赏合约为对象,分析合约中潜在的漏洞,自顶向下地对合约本身及其执行环境建立着色Petri网模型,并引入攻击者模型来考虑合约遭受攻击的情况。通过运行模型以验证合约存在交易顺序依赖漏洞,最后基于Remix平台在以太坊网络中证实结论的正确性。     

基于划分软件安全Petri网的需求形式化验证

为了解决Petri网对复杂软件系统进行形式化验证时在安全性描述、自动化程度和验证效率方面存在的不足,提出一种软件安全Petri网。扩展了库所定义,提出了安全距离及其计算方法,以增强Petri网对软件安全性的描述能力。设计了自动划分子网结合库所安全定级的递归算法,仅对与被验证需求性质相关的划分子模型进行验证以提高验证效率,同时实现库所的安全定级。设计并实现了软件安全性需求自动化建模和验证工具原型,最后给出了在典型安全关键软件--机载除冰软件系统上的应用以说明方法和工具原型的有效性。     

基于多Agent系统网管模型的形式化建模

运用多Agent系统实现分布、自治的网络管理是构造下一代网络管理系统的一条全新思路。然而,大多数基于多Agent系统的网管模型均采用非形式化的方法进行描述,容易造成人们对模型理解的歧义性和在系统开发过程中的随意性。一种利用有色Petri网对分布式网络管理模型进行形式化建模的方法被提出。利用该方法所建立的形式化模型,能够对分布式网管模型中多Agent系统的组成结构和运行机制进行全面刻画,能够描述模型中用到的Agent的各种特性。     

基于着色Petri网的GEO-RBAC策略验证

GEO-RBAC是一种能够处理空间信息的访问控制策略,其角色按照粒度分为角色模式和角色实例,按照维数分为空间角色和非空间角色。基于实例的角色分配与传统RBAC策略类似。使用着色Petri网对GEO-RBAC中基于模式的角色分配进行建模,并给出了可达性分析方法,通过对角色分配事件图可达状态的分析实现了GEO-RBAC策略的一致性验证。     

基于CPN的可信路由器发现协议建模与仿真分析

为了保证终端设备能够可信高效地通过接入路由器访问互联网,提出一种可信路由器发现协议,实现安全、高效的接入路由器身份认证过程,并基于着色Petri网(Colored Petri Nets,CPNs)为该协议建立关联的功能验证模型和性能分析模型,有效集成协议的安全性验证与性能分析过程,以确认该协议在保证安全能力的基础上可以有效提升接入路由器身份认证过程的性能。基于着色Petri网的安全性验证与性能评价集成分析方法为安全类协议的性能改进分析提供了一种更加便捷、有效的协议仿真分析方法。     

基于图规约法的TCPN工作流网模型的验证方法

针对经典Petri网的一些固有缺陷，对其在颜色、时间上进行了扩展，并结合工作流网的概念，给出了基于TCPN（Time-Color-Petri Net）的工作流网的定义。文中重点研究了采用图规约法对TCPN工作流网模型的验证，提出了流控制结构的图规约规则，并对这些规则进行了证明．在此基础上，运用这些规则对复杂工作流模型的算例进行逐步规约，验证了模型的合理性。     

基于CPN的排队网模型分析方法

提出一种新的排队网模型分析方法,将排队网络按照一定的规则转化为层次着色Petri网,利用着色Petri网的分析工具CPN-TOOLS在模型中加入Monitor监视器监视网络状态,在仿真过程中收集状态数据进行性能评价.这种方法在分析过程中不会对系统结构进行限制,可以对系统的任何方面进行评价,具有很大的灵活性;层次化模型不限制网络规模,不涉及状态空间问题可以更好的用来求解大规模的排队网络.     

基于CPN建模技术的研究

Coloured Petri Nets(CPN) 是一种面向图形的建模语言.给出了CPN的形式化定义,并以实例说明描述分布式数据库系统的一种基于CPN的方法.     

HLA仿真联邦的时间管理性能预测模型

为了预测HLA仿真联邦的时间管理性能,衡量其并行性,首先提出了着色交互Petri网,建立了HLA仿真联邦的时间管理性能预测模型;然后,应用Stateflow实现了该模型,应用模型的运行结果定量地衡量仿真联邦的并行性;最后,通过在水声对抗仿真系统中的应用,验证了模型的有效性.应用该预测模型,仿真联邦能够通过采用提高并行性的参数与策略,实现时间管理性能的提高.     

自恢复软件系统的建模与分析

不断增长的软件系统复杂性要求系统本身能够实时对资源变化、故障错误进行响应。虽然现在也发表了一些有关自恢复软件系统方面的文章，然而关于这类系统软件体系结构形式化的研究尚属起步；首先分析了自恢复功能软件的运行机制，给出了自恢复软件系统的形式化模型描述；在此基础上，对指挥控制系统（command and control system，简称c2）软件体系结构进行了形式化定义和分析。结果显示所设计的自恢复模型能够满足软件系统的约束条件，提高了系统的可用性。     

基于通信的列车控制系统的有色Petri网模型的研究

基于通信的列车控制系统是我国铁路信号技术发展的一个重要方向，在分析了基于通信的列车控制系统结构的基础上，采用有色Petri网方法对该系统进行建模仿真研究。有色Petri网是一种以图形形式描述系统结构、功能的建模分析方法，特别适合大型异步并发系统的建模与仿真。为了使模型简洁清楚，提出了分整体层、处理层和功能层三部分建立相应的系统有色Petri网图的分析方法，并用CPN／Tools工具软件进行实现。通过建立一个基于通信的列车控制系统的有色Petri网模型，为最终开发出该系统的软件仿真平台奠定了良好的基础。     

基于颜色Petri网的多agent动态调度建模与分析

多agent系统是一个典型的分布式系统,其任务调度策略的性能对于整个系统的性能有重要的影响。调度策略研究领域中一个重要问题是如何动态可视化地呈现调度过程。颜色Petri网结合了Petri网和高级程序语言的优点,拥有严格的数学理论基础,能够对分布式系统进行图形化的模拟。提出了一种基于层次颜色Petri网的多agent调度过程建模方法,该方法对多agent任务处理的全过程进行了建模,模型中通过不同角色的agent对任务进行动态分解和调度,利用Petri网仿真工具,能够在调度过程中考察所提出的调度策略与已有调度策略相比所具有的优点,而且通过对调度简化模型的状态空间进行分析,证明了调度策略的正确性和合理性。目前这种基于Petri网的形式化的可视仿真方法和模型评价方法是其它验证方法难以实现的。     

具有紧急消息的航电总线Petri网建模与性能分析

在航空电子综合化系统的设计过程中，总线系统的性能指标与整个航电系统的总体指标有着密切的关系。给出了一套完整的基于确定与随机Petri网的综合航电总线系统的性能评价的模型和算法。通过对总线系统的确定与随机Petri网模型的求解，给出了具有紧急消息的总线系统的两个重要性能指标总线负载、延迟时间，通过对性能曲线的分析，可以为综合航电系统的设计和完善提供重要的理论依据。     

BitTorrent协议的Petri网建模方法研究

BitTorrent协议被大规模文件共享、视频点播等P2P应用所广泛采用,但其交互行为复杂且并发度高,难以构建规模适度的形式模型以支持高效可行的协议功能行为分析。基于着色Petri网提出一种BitTorrent协议分层建模方法,给出协议的着色Petn网层次模型,集戍模拟、状态空间分析与模型检验等方法对模型的不同抽象层进行分析。确认协议模型有效性,并验证协议行为满足协议需求。BitTorrent协议的着色Petri网层次模型不但为协议开发提供准确、直观的形式规范说明,而且便于协议行为模拟和协议属性分析,有效缓解大规模系统建模分析过程中存在的状态爆炸问题。     

防空导弹C3I系统谓词/变迁赋色Petri网建模与仿真

介绍了Perti网概念及其标识转移方程的完整动态描述。对复杂的防空导弹C3 I空防对抗过程进行了具体分析 ,描述了某型防空导弹的具体作战过程 ,在有机结合谓词公司Petri网和赋色Petri网基础上 ,建立了基于谓词 /变迁的赋色Petri网模型 ,给出了具体的前置谓词公式。最后对仿真流程进行了描述 ,对战术级指挥控制过程的评估研究有极其重要的意义。     

自动导引车系统的有色时延PN-有向图建模

基于有色时延Petri网理论、有向图理论、PN的合成和简化技术,结合烟草行业的卷接包车间为典型实例对自动导引车系统(AGVS)进行分析,构造了AGVS的有色时延Petri网-有向图模型,包括适合于仿真软件开发的AGVS有色时延Petri网模型,适合于路径优化研究的AGVS有向图模型和从有向图模型得到有色时延Petri网模型的转换算法。利用该模型成功的开发了AGVS仿真软件系统AGVSim。     

基于赋色Petri网的离散事件系统矩阵模型与仿真

一种新的离散事件系统（DES）矩阵状态方程和Petri网的标识转移方程相结合的矩阵模型给出了完整的DES动态描述。本文介绍了一种可动态修正Petri网关联矩阵系数的矩阵模型仿真框架,解决了路径选择和调度决策问题,使这种模型可以推广到用基于赋色Petri网描述的DES仿真。     

协同VPD基于HLA的ASP平台及其联邦集成

首先讨论了HLA在集成化虚拟产品开发的协同仿真平台中的研究进展,提出了基于资源管理联邦的协同仿真平台概念,解决了单联邦的不足。在此基础上,基于网络化制造的需要,讨论了ASP平台及其联邦集成,包括其体系结构（FIA）、联邦执行支撑环境（FEI）以及解决的关键技术,实现了多个异构ASP平台联邦集成,用户可跨平台点播,自动导航;开发的联邦集成系统已在北京网络化制造工程中得到了实际应用。