从Petri网到形式描述技术和协议工程 被引量：41

1

作者 罗军舟 seu.edu.cn +1 位作者 沈俊 顾冠群 《软件学报》 EI CSCD 北大核心 2000年第5期606-615,共10页

协议是计算机网络的命脉 ,协议复杂性的提高导致了协议工程学科的出现 .该文首先分析了协议工程各项活动的内容、方法和相互关系 ,讨论了各种形式描述技术 ( formal description technique,简称 FDT)的特性及其优缺点 ,从而引出基于 Pe... 协议是计算机网络的命脉 ,协议复杂性的提高导致了协议工程学科的出现 .该文首先分析了协议工程各项活动的内容、方法和相互关系 ,讨论了各种形式描述技术 ( formal description technique,简称 FDT)的特性及其优缺点 ,从而引出基于 Petri网理论的 FDT.该文说明了 Petri网作为协议描述技术的优势 ,指出当前基于Petri网的协议工程研究的难点 ,其中面向协议开发的网工具是一项重要的研究内容 .按照开放系统互连参考模型的层次 ,总结了国际上的研究进展情况 ,并阐述了未来的研究趋势 .最后从协议描述、协议验证与分析以及辅助测试与实现这 3个角度给出了基于 展开更多

关键词 协议工程 形式描述 petri网 计算机网络

在线阅读 下载PDF 职称材料

联锁软件的Petri网形式化定义 被引量：10

2

作者 杨扬 潘明 何梅芳 《中国铁道科学》 EI CAS CSCD 北大核心 2002年第3期49-54,共6页

用Petri网对联锁系统中的核心部分———联锁机中的联锁软件进行形式化定义和分析 ,以减少联锁系统中的不确定性因素 ,降低联锁软件的复杂性 ,保证联锁软件定义的正确性 ,并对该定义进行了形式化验证。同时以进路建立过程作为事例 ,说... 用Petri网对联锁系统中的核心部分———联锁机中的联锁软件进行形式化定义和分析 ,以减少联锁系统中的不确定性因素 ,降低联锁软件的复杂性 ,保证联锁软件定义的正确性 ,并对该定义进行了形式化验证。同时以进路建立过程作为事例 ,说明了用Perti网形式化定义联锁软件的具体过程。采用分层模型化技术对联锁软件中的各个变迁 (模块 )进行逐级分解和验证 ,最终得到经过验证的、足够详细的联锁软件模型。利用该模型能对系统的一些重要性能 (如安全性和实时性 ) 展开更多

关键词 联锁软件 铁路信号 计算机联锁 petri网 形式化定义 形式化验证

在线阅读 下载PDF 职称材料

Petri网协议分析器 被引量：10

3

作者 罗军舟 顾冠群 谢俊清 《计算机学报》 EI CSCD 北大核心 1997年第3期206-212,共7页

本文以基于Ｐｅｔｒｉ网的协议工程工作站为研究目标，阐述协议工程工作站的基本功能，简介ＥＰｒ／ＴＮ网系统，着重探讨作者实现的协议描述分析辅助工具ＰＥＳＡＴ的功能特点和实现技术，并以一个例子加以说明．最后作者指出ＰＥＳＡ... 本文以基于Ｐｅｔｒｉ网的协议工程工作站为研究目标，阐述协议工程工作站的基本功能，简介ＥＰｒ／ＴＮ网系统，着重探讨作者实现的协议描述分析辅助工具ＰＥＳＡＴ的功能特点和实现技术，并以一个例子加以说明．最后作者指出ＰＥＳＡＴ的完善工作和理想协议工程工作站建立的前景． 展开更多

关键词 协议工程 petri网 网络协议 协议分析器

在线阅读 下载PDF 职称材料

基于Petri网的协议并行化处理模型的描述和验证 被引量：3

4

作者 顾冠群 姜爱泉 罗军舟 《计算机学报》 EI CSCD 北大核心 1996年第11期867-870,共4页

本文提出了一个ＯＳＩ／ＲＭ运输层协议并行处理模型，以适应协议的高效处理．根据模型特点，使用Ｐｅｔｒｉ网作为形式化描述工具，对该模型进行描述、分析和验证．

关键词 petri网 并行处理 形式化描述 形式化验证

在线阅读 下载PDF 职称材料

基于时间Petri网的密码协议分析 被引量：6

5

作者 张广胜 吴哲辉 逄玉叶 《系统仿真学报》 CAS CSCD 2003年第z1期11-16,共6页

形式化分析方法由于其精炼、简洁和无二义性逐步成为分析密码协议的一条可靠和准确的途径,但是密码协议的形式化分析研究目前还不够深入。在文中首先对四类常见的密码协议形式化分析方法作了一些比较,阐述了各自的特点,然后用时间Petri... 形式化分析方法由于其精炼、简洁和无二义性逐步成为分析密码协议的一条可靠和准确的途径,但是密码协议的形式化分析研究目前还不够深入。在文中首先对四类常见的密码协议形式化分析方法作了一些比较,阐述了各自的特点,然后用时间Petri网来表示和分析密码协议。该方法不但能够反映协议的静态和动态的特性,而且能够对密码协议进行时间、空间上的性能评估。作为实例,对Aziz-Diffie 无线协议作了详细的形式分析和性能评估,验证了已知的、存在的漏洞,并且给出了该协议的改进方案。 展开更多

关键词 密码协议 形式化分析 时间petri网 BAN逻辑 认证协议

在线阅读 下载PDF 职称材料

一种兼顾协议正确性验证和性能评估的Petri网方法 被引量：2

6

作者 范昊 吴哲辉 曾庆田 《计算机科学》 CSCD 北大核心 2005年第12期48-52,共5页

基于Petri网的协议形式化分析方法由于其精炼、简洁和无二义性逐步成为分析协议的一条可靠和准确的途径,但是协议的形式化分析目前研究还不够深入,协议分析的两个重点内容正确性验证和性能评估所需要的模型不同,一种模型只能解决一方面... 基于Petri网的协议形式化分析方法由于其精炼、简洁和无二义性逐步成为分析协议的一条可靠和准确的途径,但是协议的形式化分析目前研究还不够深入,协议分析的两个重点内容正确性验证和性能评估所需要的模型不同,一种模型只能解决一方面的工作。为了有效地解决这一问题,文中提出了一种用原型Petri网作为协议验证模型的思路和方法,在不改变原型Petri网结构的基础上对变迁赋予发生时延,解决了协议的性能评估问题。本文还给出了协议验证内容与Petri网分析方法的对应关系,并对0-1停止等待协议进行了详细的分析,最后把0-1停止等待协议的原型Petri网模型转化为时延Petri网,对协议的性能进行了评估。 展开更多

关键词 协议验证 形式化分析 时延petri网 协议性能评估 0-1停止等待协议

在线阅读 下载PDF 职称材料

基于高级Petri网的OSI网络协议形式描述 被引量：2

7

作者 顾冠群 罗军舟 《计算机工程》 CAS CSCD 北大核心 1993年第4期47-51,共5页

在全面分析OSI参考模型的基础上,建立了OSI服务模型和协议模型;然后介绍了一种高级Petri网,称为EPr/TN网系统,作为OSI网络协议的形式描述工具;最后用EPr/TN网系统形式描述了运输协议,阐明了OSI网络协议形式描述的一般方法.＊

关键词 petri网 OSI 形式描述 网络协议

在线阅读 下载PDF 职称材料

颜色Petri网的电子商务协议攻击分析方法 被引量：1

8

作者 司亚利 刘文远 卢贝 《计算机工程与设计》 CSCD 北大核心 2014年第3期814-818,840,共6页

针对现有颜色Petri网方法较少分析电子商务协议存在重放攻击的问题,提出一种基于颜色Petri网的电子商务协议攻击分析方法,用于分析协议中可能存在的攻击。给出带有攻击者的具体建模方法和分析过程,提出从不可否认证据中提取敏感信息作... 针对现有颜色Petri网方法较少分析电子商务协议存在重放攻击的问题,提出一种基于颜色Petri网的电子商务协议攻击分析方法,用于分析协议中可能存在的攻击。给出带有攻击者的具体建模方法和分析过程,提出从不可否认证据中提取敏感信息作为不安全状态的定义方法,并且采用逆向状态分析和CPN Tools仿真工具两种方法来分析颜色Petri网模型,得出协议的攻击结果。对CMP1协议进行实例分析,理论分析和实验结果表明了该方法的正确性和有效性。 展开更多

关键词 电子商务协议 形式化分析 颜色petri网 重放攻击 颜色petri网工具

在线阅读 下载PDF 职称材料

基于有色Petri网的一种密码协议的描述和分析 被引量：1

9

作者 罗志宏 王常吉 朱思铭 《计算机工程与应用》 CSCD 北大核心 2006年第23期106-108,共3页

Petri网作为一种数学工具,已被广泛应用于过程的描述、分析和验证。文章使用有色Petri网对文献[1]中提到的一种密码协议进行描述和分析,发现并验证该协议的安全缺陷。

关键词 有色petri网 密码协议 描述和分析

在线阅读 下载PDF 职称材料

一种新型的Petri网扩充模型及其在协议描述和验证中的应用 被引量：2

10

作者 李红辉 《铁道学报》 EI CAS CSCD 北大核心 1996年第S2期121-128,共8页

在数字Ｐｅｔｒｉ网（ＮＰＮ）的基础上，提出一种新型的Ｐｅｔｒｉ同扩充模型（ＮＰＮｃ）。它与ＮＰＮ相比，具有更强的描述能力，能用于复杂协议的描述。此外，本文还提出非环协议概念，并对Ｐｅｔｒｉ同理论中适当终结、活跃等概念... 在数字Ｐｅｔｒｉ网（ＮＰＮ）的基础上，提出一种新型的Ｐｅｔｒｉ同扩充模型（ＮＰＮｃ）。它与ＮＰＮ相比，具有更强的描述能力，能用于复杂协议的描述。此外，本文还提出非环协议概念，并对Ｐｅｔｒｉ同理论中适当终结、活跃等概念进行了扩充修改。文中后部以ＯＳＩ会话协议为例说明ＮＰＮｃ模型在协议描述和验证中的应用。 展开更多

关键词 petri网 协议 描述 验证 NPN_c

在线阅读 下载PDF 职称材料

Petri网图形的压缩存储与自动转换 被引量：2

11

作者 党华锐 《微电子学与计算机》 CSCD 北大核心 1996年第1期44-47,共4页

本文给出了一种Ｐｅｔｒｉ网的计算机表示方法以及其图形的压缩存储／还原算法，并在此基础上对Ｐｅｔｒｉ网图形进行自动转换以产生此图的矩阵表示，这为在其上进行可达性分析和验证的自动化提供了极大的方便。

关键词 petri网 形式描述 通信协议 图形压缩存储

在线阅读 下载PDF 职称材料

一种基于有色Petri网的安全协议分析方法研究 被引量：2

12

作者 苏桂平 孙莎 《微型机与应用》 2011年第15期1-3,7,共4页

利用有色Petri网建模工具CPN tools中的查询函数对安全属性进行描述,搭建一个能够覆盖大部分安全性质的CPN查询函数库,提出一种基于CPN的通用和规范的安全协议形式化分析语言,该语言可以像用面向对象编程语言编程一样对安全协议进行建模。

关键词 有色petri网 安全协议 形式化分析 面向对象编程语言

在线阅读 下载PDF 职称材料

基于时延Petri网的密码协议分析及性能评估 被引量：1

13

作者 张广胜 《计算机工程与应用》 CSCD 北大核心 2003年第30期158-161,共4页

形式化分析方法由于其精炼、简洁和无二义性逐步成为分析密码协议的一条可靠和准确的途径,但是密码协议的形式化分析研究目前还不够深入,针对这一现状,该文提出用时延Petri网来表示和分析密码协议。该模型不但能够反映协议的静态和动态... 形式化分析方法由于其精炼、简洁和无二义性逐步成为分析密码协议的一条可靠和准确的途径,但是密码协议的形式化分析研究目前还不够深入,针对这一现状,该文提出用时延Petri网来表示和分析密码协议。该模型不但能够反映协议的静态和动态的特性,而且能够对密码协议进行时间、空间上的性能评估。作为实例,文章对MSR无线协议作了详细的形式分析和性能评估。最后,与其它形式化分析密码协议的方法作了比较。 展开更多

关键词 密码协议 形式化分析 时延petri网 BAN逻辑 认证协议

在线阅读 下载PDF 职称材料

基于高级Petri网的X.25/FR开放系统互连网关的描述与验证及实现

14

作者 沈金龙 潘理 孙亚民 《南京理工大学学报》 EI CAS CSCD 1998年第6期532-535,共4页

在构造 X.2 5 / FR互连网关时 ,采用 OSI有关协议。利用一种高级 Petri网(EPr/ TN)作为形式化的描述工具建立互连网关的系统模型 ,对网关中的协议转换和数据通信过程进行描述、分析和验证 。

关键词 网络互连 网关 协议 petri网 EPr/TN网系统

在线阅读 下载PDF 职称材料

交互式Petri网图形系统的设计与实现

15

作者 党华锐 赵慧 《小型微型计算机系统》 CSCD 北大核心 1995年第7期21-25,共5页

本文介绍了一种交互式Ｐｅｔｒｉ网图形系统的设计思想与实现细节，其中包括系统功能；Ｐｅｔｒｉ网的数据结构以及其图形的压缩存储／还原算法；从Ｐｅｔｒｉ网图形到其矩阵表示的自动转换等。

关键词 petri网 通信协议 图形系统 设计

在线阅读 下载PDF 职称材料

基于Petri网的MMS服务描述、验证及实现

16

作者 费翔 顾冠群 吴介一 《东南大学学报（自然科学版）》 EI CAS CSCD 1997年第2期83-89,共7页

利用Ｐｅｔｒｉ网这一形式化描述工具建立了ＭＭＳ（制造报文规范）体系结构的抽象模型，并利用Ｐｒ／Ｔ网对其中的重要服务——程序唤醒服务进行了描述、分析和验证，最后，以此为基础在ＭＡＰ、ＢＩＴＢＵＳ网上实现了ＭＭＳ服务。

关键词 petri网 计算机集成制造 制造报文规范 Pr/T网

在线阅读 下载PDF 职称材料

从协议Petri网到Estelle的转换

17

作者 罗军舟 杨晓燕 《系统仿真学报》 CAS CSCD 2003年第z1期78-82,共5页

Petri网和Estelle是国际上流行的两种描述通信协议的形式技术。基本Petri网及其衍生变种具有图形的直观表示和数学的分析方法,在协议工程领域有着广泛的应用。而Estelle类似于程序语言,可对协议进行无二义的描述。本文针对现有Petri网... Petri网和Estelle是国际上流行的两种描述通信协议的形式技术。基本Petri网及其衍生变种具有图形的直观表示和数学的分析方法,在协议工程领域有着广泛的应用。而Estelle类似于程序语言,可对协议进行无二义的描述。本文针对现有Petri网系统的不足,从协议形式描述的角度出发,定义了一种抽象通信特性的协议Petri网,给出了由协议Petri网转换为Estelle形式的方法。基于此方法文章还构造了自动实现转换的算法,并给出了一个实例。 展开更多

关键词 协议petri网 ESTELLE 形式描述技术之转换 协议描述

在线阅读 下载PDF 职称材料

网络协议工程中的Petri网技术

18

作者 冷淑霞 巨同升 《山东理工大学学报（自然科学版）》 CAS 2005年第1期84-87,共4页

按照OSI/RM模型的层次,论述了Petri网在网络协议工程中的研究进展情况,并从协议描述、协议验证与分析的角度给出了基于Petri网的协议工程的基本方法,最后用有色Petri网对数据链路层的Stop and Wait通信协议进行描述分析.

关键词 有色petri网 网络协议 协议工程 数据链路层 协议验证 描述 通信协议 OSI/RM 对数 角度

在线阅读 下载PDF 职称材料

有色Petri网的一种密码协议建模分析

19

作者 罗志宏 朱思铭 《现代计算机》 2006年第2期64-67,共4页

密码协议是任何安全系统的基础,对它的设计越来越受到广大用户的关注。本文详细论述了文献[1]提到的一种密码协议,并使用有色Petri网对该协议建模分析,说明该设计的正确性。

关键词 有色petri网 密码协议 建模 形式化分析 建模分析 安全系统

在线阅读 下载PDF 职称材料

基于染色Petri网的BGP连接过程模型 被引量：2

20

作者 王文化 沈庆国 +2 位作者 韩春永 王滨 戴三明 《计算机工程》 CAS CSCD 北大核心 2011年第6期82-84,共3页

边界网关协议(BGP)缺少形式化分析,为此,根据RFC 1771,针对2个BGP路由器间连接建立过程,使用染色Petri网建立层级模型。通过交互式仿真观察所建模型行为和预期行为是否发生偏离。判定行为偏离发生的原因,修改模型直到偏离消失。求解模... 边界网关协议(BGP)缺少形式化分析,为此,根据RFC 1771,针对2个BGP路由器间连接建立过程,使用染色Petri网建立层级模型。通过交互式仿真观察所建模型行为和预期行为是否发生偏离。判定行为偏离发生的原因,修改模型直到偏离消失。求解模型的状态空间,并验证BGP连接过程的无死锁性和公平性。 展开更多

关键词 边界网关协议 形式化模型 染色petri网 协议验证

在线阅读 下载PDF 职称材料