| 题
目 |
作
者 |
摘
要 |
| 某类有界时序Petri网的原型网形式的转化 |
刘
勇
吴 哲 辉 |
时序Petri网是对原型Petri网模型（称为时序Petri网的基网）加上时序逻辑公式进行的扩充。本文初步讨论了时序Petri网的语言表达能力，得出的结论是这种扩充不弱于带抑止弧的Petri网的表达能力，但控制型有界时序Petri网的描述能力则同有界原型Petri网是等同的。文中给出了把控制型有界时序Petri网转化为有界原型Petri网的算法，并通过实例描述了转化过程。 |
| 基于活标识性质的活网子类划分 |
吴
俊
罗
军 舟
吴
哲 辉 |
现有的Petri网子网分类在活性判断问题上难度跳跃过大，难以取得突破。通过对活标识单调性质的研究对结构活网进行了子类划分，将结构活网划分为严格单调活网、单调活网、关于冲突源单调活网、广义单调活网和奇异活网。同时，文中还给出了严格单调活网和单调活网的判定条件。这种划分对活性判断问题作了更细的分级，为活性的研究提供一种新思路。 |
| Petri网进程的描述方法研究综述 |
曾
庆 田
范
昊
吴 哲 辉 |
综述了我们在Petri网的进程研究方面所取得的成果，完整地给出了Petri网进程描述方法的体系。详细阐述了Petri网的满进程、Petri网的基本进程段、Petri网的进程表达式、Petri网的进程网系统等概念。给出了Petri网基本进程段的划分标准，证明了任意Petri网的基本进程段集是一个有限集。分别研究了有界Petri网、无界公平Petri网和任意无界Petri网的进程表达式,给出了与进程表达式描述能力等价的Petri网的进程网系统的概念,研究了进程系统的语言表达式同原系统的进程表达式之间的一一对应关系。 |
| Petri网共享子网合成活性分析 |
夏
传 良
焦
莉
陆 维 明 |
为解决子系统共享问题，提出了经由Petri网系统共享一种子网构成共享子网合成网的解决方案；给出了一种关于Petri网的从抽象化到精细化描述方法，它是使合成网保持原网性质的一种关键技术。研究了共享子网合成网的性质，提出了共享子网合成网保持有界性和活性的充分条件或充要条件；目前存在的合成方法大多对状态机、标识图或非对称选择网（AC）等进行合成，用于解决资源共享问题，而本文的方法可对一般的Petri网进行合成，解决子系统共享问题。本文的结果可为Petri网系统合成性质的考察提供有效途径，为Petri网复杂大系统的分析提供重要手段。 |
| Petri网系统的可达性分析 |
吴
文 渊
曾
振 柄 |
对Petri网系统的可达性问题做了综合性的阐述和分析,
提出了利用能量优化方法来解决可达性问题的方法,
并在此基础上结合计算代数方法和神经计算模型对可达性问题做了进一步的研究.
主要工作包括:
1.给出了Petri网到线性空间的映射规则及其可达性的等价性定理;
2.建立了能量优化模型,
将可达性判断化为优化问题;
3.用神经网络来求解能量优化模型;
4. 最后综合了计算代数方法和能量优化模型的优点给出一个基于计算代数和神经计算的方法.
作者提出了一种利用基于硬件的大规模并行的神经计算来代替基于软件的串行的数字计算的可达性判断的解决方案. |
| 广义有界上下文无关语言与Petri网语言 |
张
继 军
吴 哲 辉 |
提出了广义有界上下文无关语言的概念，该类语言是上下文无关语言的真子集；证明了广义有界上下文无关语言与上下文无关Petri网语言的等价性；进一步给出了上下文无关Petri网语言的一种形式描述——上下文无关Petri网语言表达式,对上下文无关Petri网语言给出了较完整的结构特征。
|
| 库所组合有色网－一种新型的有色网 |
霍
金 健
袁 崇 义
屈 婉 玲 |
为了解决用Petri网描述复杂系统时出现的“节点爆炸”问题，本文提出了四种特殊的弧：约束弧，柔性弧，组合弧和因果弧。库所组合有色网就是在有色网的基础上添加这四种特殊的弧得到的，这种网系统并没有增加描述能力，但在描述具有组合效果的系统时具有强大的先天优势。本文通过为电梯控制系统建模示例了这四种弧为简化模型带来的便捷之处。 |
| 几类合成网的性能分析 |
许
安 国
赵
义 军 |
研究了T-图，P-图，CFR网（无冲突可重复网）的同步合成网与共享合成网的结构性质和动态性质，这些工作对T-图网系统，P-图网系统，CFR网系统（无冲突可重复网系统）合成的性能分析提供了有力手段。 |
| 一类区间速率连续Petri网的可达稳态分析 |
廖
伟 志
文
瑛
王
汝 凉 |
连续Petri网已被证明为诸多系统的有效描述工具，而系统性能分析与连续Petri网的稳态有密切关系。本文讨论了一类区间速率连续Petri网(Interval
speed Continuous Petri Nets,简称ICPN)的可达稳态问题。通过分析区间速率连续Petri网的使能与引发语义证明了一类区间速率连续Petri网在最大引发模式下可达稳态的有关定理。研究表明这类区间速率连续Petri网在最大引发模式下其可达稳态及最终速率仅与各个迁移的区间速率有关,而与初始标识无关,从而避免了因构造演变图而产生状态爆炸的问题 |
| 最大速度恒定的连续Petri网(CCPN)的性质判定及分解 |
王
培 良
赵 义 军 |
对最大速度恒定的连续Petri网（CCPN）的结构有界性、守恒性、公平性进行了定义，并给出了判定定理。进而定义了最大速度恒定的连续Petri网（CCPN）的两种分解，并证明了这两种分解保持网的一些结构性质。 |
| MPI集群通信函数的Petri网模型 |
崔
焕 庆
吴 哲 辉
井 艳 芳 |
研究并行程序的验证问题对于提高并行编程的效率具有十分重要的意义，本文在[1]的基础上，建立了目前普遍使用的基于消息传递的并行程序编写标准之一——消息传递接口（MPI）的集群通信函数的Petri网模型，从而为进一步研究MPI并行程序的Petri网模型及其性质奠定了基础。 |
| 满足2PL协议的无死锁事务并发控制Petri网模型 |
孙
琳
吴 哲 辉
崔 焕 庆 |
在建立满足2PL协议的数据库事务并发控制的Petri网模型后，通过分析资源的调度过程得到可能产生死锁的资源集，在模型上对其进行控制，从而得到无死锁的满足2PL协议的事务并发控制的Petri网模型。 |
| 下一代移动IPv6在WLAN内快速切换的性能研究 |
杨
文 川
王
济 世
杨
巍
杨
超
刘
驰 |
通过研究下一代移动IP（MIPv6）在WLAN内的快速切换。IEEE的“Mobile
IPv6 Fast Handovers for 802.11 Networks”草案提出了一种快速切换的思想，通过链路层传递切换信息，经过对其进行改进，将第三层的切换决策权交给网络（而不是移动节点），成功的实现了第二层和第三层的切换并进，从而大大降低了切换时延，提高了系统的效率。该切换算法在OPNET仿真环境下模拟实现，效果甚佳。
|
| 基于颜色Petri网的TCP协议模拟和分析
|
徐
誉 尹
吴 哲 辉 |
TCP协议是目前广泛使用的一种可靠的网络传输协议。TCP协议的分析和改进一直是研究的热点，由于协议的复杂性，协议的形式化描述是其中的难点。文章用颜色Petri网及其工具CPN/tool对简化的TCP协议进行建模和分析，对协议中各种动态关系有较好的刻画，分析了协议的不足，减少了利用一般Petri网系统（如P/T系统）模拟复杂系统的难度。
|
| AB协议的Petri网描述与J2ME可视化实现 |
臧
广 良
郑
进 远
李
祥 |
在J2ME(Java
2 Mobile Edition)开发环境—J2ME
Wireless Toolkit中，研究了Robert
Esser[1]的Petri网开发软件包，在手机（或其他手持移动设备）上实现Petri网的可视化设计的原理，实现了著名的AB（交替比特）通信协议[6]，并对该软件包的若干功能进行了改进。 |
| 基于PWF_nets的服务组合方法 |
喻
坚
杨
萍
黄 鹂 鸣 |
针对使能最终用户直接组合服务生成个人应用的问题，提出一种基于Petri网模型：WF_logic，WF_semantics，WM_logic和WM_semantics（统称为PWF_nets）的服务组合方法。该方法可以指导最终用户在不同的抽象等级逐步为服务组合流程的逻辑、语义和管理建模，使最终用户在不同的阶段专注于服务组合的不同方面并且在每个阶段都有合适的网模型支持，不仅可以提高其构造合理有效应用的成功率，而且各个阶段建立的模型也可以被形式验证。 |
| 扩展时间戳状态类 |
潘
理
李
文 军
刘
显 明 |
状态类方法是时间Petri进行可达性分析的主要方法.提出扩展时间戳状态类方法,该方法通过扩展变迁的同步使能信息到时间戳状态类,
解决了时间戳状态类方法中同步使能变迁的可实施性问题。最后以一个典型生产系统为例展示扩展时间戳状态类方法的应用。 |
| 密码协议的p
-网形式化描述和分析 |
曹
木 亮
吴 智 铭
杨 根 科 |
p
-网是一类模块化的、具有代数演算功能的高级Petri网。通过引入项、buffer库所和解密变迁等建模元素，本文在p
-网中建立了密钥管理和加密信息的传输机制，形成了密码协议的Petri网形式化模型，而且对于任意的一个密码协议，都可以将其模块化，本文还提出了密码协议的鉴别性和安全性的验证机制。通过对Needham-Schroeder协议的实例分析，对密码协议的密钥交换和鉴别性,
以及协议存在的漏洞,进行了有效的形式化描述和分析 |
| 基于Petri网的强制访问控制模型及其安全分析 |
蒋
屹 新
林
闯
封
富 君
尹
浩 |
强制访问控制模型（MAC）是一种重要的安全模型。在多级安全的格模型和Bell-LaPadula安全模型的基础上，对MAC安全模型进行了形式化描述，并给出了与其等价的着色Petri网模型。在Petri网状态可达图的基础上，对MAC模型的有关安全属性，如主体访问客体的时序关系，主体访问的可达性，因主体的动态安全级访问而存在的安全隐患以及因主体对客体的间接访问而导致敏感信息的可推测性等进行了较为详细地分析。通过对一个安全模型的范例分析，结果表明：基于Petri网的安全模型的分析方法可以充分利用现有的可达图的分析方法来对系统安全模型的有关性质进行分析和验证，能够在安全模型的设计和实现阶段有效地改善系统的总体安全策略。 |
| 不可否认协议形式化分析的Petri网方法 |
黎
波 涛
罗 军 舟 |
Petri网是一种描述及分析并发行为的工具，在安全协议的形式化分析中得到了广泛的应用，但目前还没有人使用Petri网来分析不可否认协议。本文以一般安全协议的Petri网分析方法为基础，提出了使用Petri网分析不可否认协议的建模及分析方法，该方法可以描述并分析一些其它形式化方法无法描述的协议性质。使用该方法分析J.
Zhou和D.
Gollmann的公平不可否认协议发现了它议的一个许多其它形式化方法不能发现的已知缺陷。
|
| 基于BPEL4WS和Petri网的服务建模与分析 |
王
艳 春
林 广 艳 |
描述了SQA中基于BPEL4WS（Business
Process Execution Language for Web Services)和Petri网的服务建模与分析方法，提出了将基于BPEL4WS的业务流程建模转化为Petri网模型的方法，并在此基础上结合实例，对所得的Petri网模型进行分析，从而验证服务模型的安全性、死锁、循环等方面是否符合要求。 |
| 基于Petri网的认证协议分析 |
董
卫
吴 哲 辉 |
认证协议的成功设计是网络安全领域的关键问题之一，对其进行形式化分析是当前研究的热点。在已知协议的运行模式的基础上，给出了基于Petri网的认证协议分析的具体方法，并通过一个实例说明了该方法的有效性。 |
| Petri网在工作流系统建模和分析中的应用 |
庞
善 臣
蒋
昌 俊 |
工作流技术是计算机应用领域的一个研究热点，而行之有效的建模方法和分析工具是工作流系统的关键，也是研究人员的研究重点。介绍工作流系统的Petri网、时间Petri网、逻辑Petri网、着色Petri网、随机Petri网等建模方法，对基于工作流网（WF-net）的完整性验证、性能分析、资源调度、时间分配以及协同分析等方法进行综述，指出Petri网在工作流建模和分析中的不足，提出了Petri网解决工作流系统建模和分析进一步的研究的内容。 |
| 基于扩展任务结构的工作流建模及分析 |
邢
光 林
洪
帆
朱
贤 |
任务结构是工作流管理系统中常用来进行工作流建模的语言，但其核心是过程控制流方面的规范，对其他方面很少涉及，比如活动间的信息流、时间约束等等。本文首先对任务结构进行了扩展，加入了资源和多粒度时间的概念，使其除了能描述任务的相关性外，也能很好地模拟任务间的信息流以及由于流程的分布性等因素而引起的多粒度时间约束。接下来对扩展任务结构的多粒度时间约束一致性和合理性进行了分析和验证。 |
| 基于随机Petri网的工作流服务时间的等价计算方法 |
田
立 勤
陈
福 明 |
工作流模型的性能研究越来越受到人们的重视[1-4]，随机Petri网易于描述分布、并发和异步等特征，加上它具有坚实的数学分析基础，在工作流的模型中独具鳌头。但随机Petri网在表示实际工作流模型时常常会出现状态空间爆炸的问题，所以如何得到一个与原模型等价的、紧凑的模型一直是研究模型的重要内容之一。从简单的由两个模块组成的基于随机Petri模型的工作流系统分析开始，论述了如何计算化简后的、与原工作流基本模型等价的服务时间的概率密度。有了概率密度就很容易计算它的期望值、方差等随机变量的数字特征，这就为求化简后的工作流模型的等价性能打下理论基础。由于这些公式具有通用性，所以只要根据工作流实际情况确定模块服务时间的概率分布（如指数分布），就可以求出与该类工作流模型等价的服务时间了。最后以工作流模块服从指数分布为例，利用上面得出的公式计算出了这类工作流的等价概率密度和服务时间，进而简化了模型，同时本文的结果也为实际模型的性能等价化简奠定了坚实的理论基础。 |
| 基于Petri网的分层工作流模型研究 |
张
亮
姚 淑 珍 |
为了满足企业对过程模型在描述能力和分析能力上的要求，提出了一个基于Petri网的分层工作流过程模型。在深入分析各种工作流模式的基础上，对基本网的进行了一些的扩展，通过增加变迁入口函数，变迁体函数，消息机制，控制变量等，描述了工作流模式中的多实例，取消，高级同步等复杂模式。给出了工作流过程的描述模型DWF_net和分析模型AWF_net的形式化定义。描述模型DWF_net实现对各种复杂流程的直接描述。变迁入口函数通过对控制变量的判断，来消解DWF_net中的冲突。变迁体函数通过可扩展逻辑描述语句，来实现对控制变量的读写及收发消息等操作。AWF_net作为DWF_net的分析模型，剥离了DWF_net个案的语义信息，可以直接利用已有的Petri网分析技术来分析模型。最后，通过一个综合实例来说明如何使用本文提出的模型来对各种复杂流程建模和分析。 |
| 基于Petri网和抽象方法的工作流模型分解 |
封
富 君
林
|
