共查询到20条相似文献,搜索用时 156 毫秒
1.
基于Petri网的联锁软件测评仿真建模 总被引:1,自引:0,他引:1
车站联锁软件一直有着严格的测试要求,仿真模块是软件测试的重要组成部分,Petri网作为形式化语言的一种,有着准确与完备的特点,对于联锁软件这类安全苛求软件的测试尤为适合,提出了一种使用Petri网对联锁软件测试中仿真模块建模的方式,并分别给出了用基本Petri网和有色Petri网的2个建模实例.该模型有助于提高铁路联锁软件测试系统的安全性与精确性. 相似文献
2.
GONG Jie 《数字社区&智能家居》2008,(30)
车站联锁软件一直有着严格的测试要求,仿真模块是测试的重要组成部分,Petri网作为形式化语言的一种,有着准确与完备的特点,对于安全苛求软件的测试尤为适合,该文提出了一种使用Petri网对联锁软件测试中仿真模块建模的方式,并分别给出了针对铁路道岔的基于基本Petri网和有色Petri网2个建模实例。该模型有助于提高测试系统的安全性与精确性。 相似文献
3.
4.
使用统一建模语言(unified modeling language,UML)为联锁软件建立平台无关的模型(platform independent model.PIM),可以实现在异种平台间的移植和复用,并有助于自动生成测试案例和测试脚本。UML建模包括静态结构分析和动态行为分析。Petri网可对联锁软件与安全性相关的动态行为精确和严格地进行形式化描述。 相似文献
5.
Petri网是描述并发系统的很直观的图形工具Spin是一种著名的分析验证并发系统性质的工具。本文首先论述Petri网性质的线性时序逻辑描述,研究用Promela编程描述Petri网和用Spin对Petri网性质进行检验的方法,最后通过两个具体的示例说明这种方法是成功的。 相似文献
6.
网上证券交易系统的时序Petri网描述及验证 总被引:9,自引:0,他引:9
基于时序Petri网对我国现行网上静态和动态证券交易系统进行了模拟、形式描述及功能正确性验证.应用时序逻辑推理规则,从形式上严格证明了证券交易系统需求规范及其时序Petri网模型动态行为的一致性.结果表明,时序Petri网能够清楚而简单地描述事件间的因果关系和时序关系以及并发系统中某些与时间有关的重要性质,如最终性和公平性.因此,时序Petri网可作为并发系统形式化描述和分析的有力工具. 相似文献
7.
综合航电系统是一种对可靠性、实时性要求非常高的嵌入式应用系统。为了解决针对复杂应用场景下综合航电系统的处理时间和工作时序预估较困难、且计算自动化程度不高等测试验证问题,提出了一种基于时间约束Petri网的综合航电系统时序验证和分析方法。给出了时间约束Petri网的形式化定义,分析了综合航电系统工作流程中各节点的时间属性,通过引入时序约束路径的概念,并提出了时序推理算法。通过在仿真算例中进行计算并对比实际运行数据,结果表明该方法在针对综合航电系统运行时序的验证分析方面具有有效性。 相似文献
8.
Petri网是计算机异步成分之间进行通信的理论基础.Petri网的应用涉及计算机学科的各个领域.文中运用Petri网工具来对工作流技术进行了详细的分析与描述,并用一个例子来说明如何使用Petri网来描述工作流的各种同步关系以及流向,最后,文章还给出了一个由功能模型、数据/信息模型、组织模型、资源模型组成的工作流复合模型. 相似文献
9.
时序逻辑电路设计的Petri网方法 总被引:2,自引:0,他引:2
1 引言 Petri网是一种系统模拟和分析的工具,它可以揭示出被模拟系统在结构和动态行为方面信息,利用这些信息可以对被模拟系统进行性能评估并提出改进系统的建议,从而设计出一个高质量的实际应用系统。文[1,2]利用Petri网的特性分别给出了组合逻辑电路和时序电路的Petri网分析方法,其基本思想是将已设计好的逻辑电路转化成Petri网,利用Petri网的各种分析方法(可达树、状态矩阵)进行分析。时序电路的设计是分析方法的逆过程,是根据给定的状态图或通过对设计要求的分析得到的状态图,设计出时序电路的过程;时序逻辑电路可分为同步和异步,然而采用传统的时序电路的设计方法时,即使是同步时序电路的设计也需要 相似文献
10.
并发程序验证的时序Petri网方法 总被引:10,自引:0,他引:10
并发程序的设计、分析和验证已经成为计算机理论界基础理论研究的方向之一。Petri网和时序逻辑被认 为是探讨该问题较为有效的两个理论工具,但二者都有局限性。该文引用一种新网子类;时序Petri网,描述了并发程序的时序Petri网建模方法;利用网结构描述程序基本框架及保证语句的原子性,通过时序逻辑公式反映程序的共享逻辑变量的赋值变化及时序关系,从而有效地对基本网无法描述的并发程序进行了建模;在此基础上,结合Petri网的可达图分析技术和时序逻辑的演绎公式,分析和验证了并发程序的安全性和活性性质。 相似文献
11.
12.
一种基于线性逻辑的Petri网分析方法 总被引:2,自引:0,他引:2
1 引言 Petri网是一种用网状图形表示系统模型的方法,能够从组织结构、控制和管理的角度,精确描述系统中事件(变迁)之间的依赖(顺序)和不依赖(并发)关系。Petri网理论提供了强大的分析方法,如不变量分析、系统性能分析(如活性)等以证明系统的正确性。近年来Petri网也被用来表示知识推理,例如用于诊断和监控,这就需要发展一种关于Petri网行为的推理主题。有些学者把经典逻辑和Petri网相结合,用Petri网表示产生式规则系统,网的框架代表基于产生式规则 相似文献
13.
基于Petri网的联锁软件安全性测试的研究 总被引:2,自引:0,他引:2
安全是铁路运输生产永恒的主题。联锁软件是保障铁路车站列车或机车(以下简称列机车)作业安全的关键软件,充分的测试对于保证其安全性具有举足轻重的作用。文章在分析文献[1][5][6]的联锁软件安全性需求故障树模型的基础上建立了联锁软件安全性需求的Petri网模型,提出了一种基于十字链表的Petri网的存储结构,给出了一种求解割集的算法实现;接着简述了安全性测试用例的自动生成方法;最后给出了该方法在HJ04A系统联锁软件安全性测试中的应用。 相似文献
14.
利用自动机理论模型检验算法,检验车站联锁逻辑的有色Petri网模型是否满足预期的性能。通过采用带标签的广义Büchi自动机(LGBA)构建线性时态逻辑,有效地解决了模型检验中的状态空间爆炸问题。该方法的研究增强了有色Petri网的分析和验证能力,利用该方法对车站联锁逻辑的实际问题进行了性能验证。 相似文献
15.
不可否认协议的Petri网建模与分析 总被引:6,自引:0,他引:6
Petri网是一种描述及分析并发行为的工具,在安全协议的形式化分析中得到了广泛的应用.作为一种特殊的安全协议,不可否认协议虽然已得到了多种形式化方法的分析,但还没有人使用Petri网来分析它们.以一般安全协议的Petri网分析方法为基础,提出了使用Petri网分析不可否认协议的建模及分析方法,该方法可以描述并分析一些其他形式化方法无法描述的协议性质.使用该方法分析Zhou和Gollmann于1996年提出的一个公平不可否认协议,可以发现该协议的一个许多其他形式化方法不能发现的已知缺陷. 相似文献
16.
模糊时间Petri网的时间推理及其在过程监测中的应用 总被引:2,自引:0,他引:2
针对传统分析方法的不足,提出用线性逻辑给出模糊时间Petri网描述和时间推理的方法。该方法能清楚地分析模糊时间Petri网的运行行为,具体例子说明了其在系统过程监测和诊断中的应用。 相似文献
17.
18.
19.
20.
Petri网是一种用网状图形表示系统模型的方法,它能够从组织结构、控制和管理的角度,精确描述系统中事件(变迁)之间的依赖(顺序)和不依赖(并发)关系。但传统的Petri网理论其不足之处在于:它的分析方法主要是可达树分析法和线性代数描述法。可达树分析法是针对某一个初始标识的,一个新的初始标识就意味着需要重新构造可达状态图;当系统存在较多 相似文献