共查询到18条相似文献,搜索用时 468 毫秒
1.
网上证券交易系统的时序Petri网描述及验证 总被引:9,自引:0,他引:9
基于时序Petri网对我国现行网上静态和动态证券交易系统进行了模拟、形式描述及功能正确性验证.应用时序逻辑推理规则,从形式上严格证明了证券交易系统需求规范及其时序Petri网模型动态行为的一致性.结果表明,时序Petri网能够清楚而简单地描述事件间的因果关系和时序关系以及并发系统中某些与时间有关的重要性质,如最终性和公平性.因此,时序Petri网可作为并发系统形式化描述和分析的有力工具. 相似文献
2.
3.
基于时序Petri网的联锁逻辑形式建模与验证 总被引:1,自引:0,他引:1
时序Petri网结合Petri和时序逻辑的优点,清晰简洁地描述并发系统事件间的时序和因果关系,包括系统的最终性和公平性。文章给出安全苛求系统——车站信号联锁逻辑系统的时序Petri网描述,并使用时序逻辑描述系统状态的时序和因果关系,最后通过分析和验证模型的性质得出系统是正确的。 相似文献
4.
Petri网是描述并发系统的很直观的图形工具Spin是一种著名的分析验证并发系统性质的工具。本文首先论述Petri网性质的线性时序逻辑描述,研究用Promela编程描述Petri网和用Spin对Petri网性质进行检验的方法,最后通过两个具体的示例说明这种方法是成功的。 相似文献
5.
并发程序验证的时序Petri网方法 总被引:10,自引:0,他引:10
并发程序的设计、分析和验证已经成为计算机理论界基础理论研究的方向之一。Petri网和时序逻辑被认 为是探讨该问题较为有效的两个理论工具,但二者都有局限性。该文引用一种新网子类;时序Petri网,描述了并发程序的时序Petri网建模方法;利用网结构描述程序基本框架及保证语句的原子性,通过时序逻辑公式反映程序的共享逻辑变量的赋值变化及时序关系,从而有效地对基本网无法描述的并发程序进行了建模;在此基础上,结合Petri网的可达图分析技术和时序逻辑的演绎公式,分析和验证了并发程序的安全性和活性性质。 相似文献
6.
通信顺序进程(CSP)和Petri网是两种重要的并发系统建模工具。CSP语言具有高度抽象性,可有效刻画并发进程之间的各种相互作用,但在物理结构的描述与验证分析方面显得不足。Petri 网是一种形式化、图形化的并发系统建模和分析工具,侧重于系统的物理结构描述和性质分析。结合两者优点,首先利用CSP描述待验证的并发系统,然后将其转化为Petri网来分析系统的动态行为特性,最后利用性质分析工具TINA对系统性质进行分析和验证。实验结果表明,传统的CSP进程性质验证工具不能验证CSP进程的安全性,但其转化为Petri网后可有效地分析出导致安全性不能满足的危险因素,从而扩大了CSP描述的并发系统可验证性质的范围。 相似文献
7.
8.
以输送机器人生产线控制系统设计为例,提出将基于Petri网的Stateflow建模仿真方法应用于PLC控制软件的开发过程中。首先利用Petri网对系统控制功能进行分析,结果表明系统在运行时序上存在并行冲突,采用Petri网的数学建模功能协调冲突后,通过可达图验证了此Petri网模型是安全无死锁的;其次在上述基础上将Petri网与Stateflow组成元素相对应并进行转换;最后利用Simulink构建模型进行系统仿真分析,证明输送机器人生产线控制逻辑正确,状态转移有效。 相似文献
9.
10.
UML缺乏精确的语义,难以对其所表示的系统进行形式化分析和一致性检验.为了使UML能够更精确地对系统模型进行描述,学者们提出了一些形式化的方法.论文对比分析了用Petri网、时序逻辑XYE/E和动态描述逻辑形式化UML状态图的方法,指出了它们各自的优缺点以及应用领域. 相似文献
11.
Zhenhua Duan Hanna Klaudel Maciej Koutny 《The Journal of Logic and Algebraic Programming》2013,82(2):95-110
interval temporal logic (itl) and Petri nets are two well developed formalisms for the specification and analysis of concurrent systems. itl allows one to specify both the system design and correctness requirements within the same logic based on intervals (sequences of states). As a result, verification of system properties can be carried out by checking that the formula describing a system implies the formula describing a requirement. Petri nets, on the other hand, have action and local state based semantics which allows for a direct expression of causality aspects in system behaviour. As a result, verification of system properties can be carried out using partial order reductions or invariant based techniques. In this paper, we investigate a basic semantical link between temporal logics and compositionally defined Petri nets. In particular, we aim at providing a support for the verification of behavioural properties of Petri nets using methods and techniques developed for itl. 相似文献
12.
Yu-YueDu Chang-JunJiang 《计算机科学技术学报》2004,19(2):0-0
Temporal colored Petri nets, an extension of temporal Petri nets, are introduced in this paper. It can distinguish the personality of individuals (tokens), describe clearly the causal and temporal relationships betwee nevents in concurrent systems, and represent elegantly certain fundamental properties of concurrent systems, such as eventuality and fairness. The use of this method is illustrated with an example of modeling and formal verification of an online stock trading system. The functional correctness of the modeled system is formally verified based on the temporal colored Petri net model and temporal assertions. Also, some main properties of the system are analyzed. It has been demonstrated sufficiently that temporal colored Petri nets can verify efficiently some time-related properties of concurrent systems, and provide both the power of dynamic representation graphically and the function of logical inference formally. Finally. future work is described. 相似文献
13.
14.
Petri网和统一建模语言UML是当前工作流建模领域两种非常流行、功能强大的建模工具。Petri网便于描述,可以动态地运行,但缺乏层次;UML可以完整、细致地刻画系统,但量化不够,缺乏有效、严密的分析工具与方法。本文整合两种建模方法的优点,提出一种集成U.P建模的方法,该方法能够有效地描述系统,实现系统的模块化和模型重用,还能够对系统进行严密的分析,通过对模型仿真,找出其缺,羔和不足。 相似文献
15.
16.
Temporal Petri nets are Petri nets in which certain restrictions on the firings of transitions are represented by formulas containing temporal operators. The use of temporal Petri nets for formal specification and verification of the alternating bit protocol is discussed. The temporal Petri net which models the protocol is analyzed formally using the existing theory of ω-regular expressions and Buchi-automata 相似文献
17.
基于有色网的多Agent计划建模 总被引:1,自引:0,他引:1
有色网能够描述资源和操作的具体语义。首先,由于计划中的操作和状态的个数的有限性,与有色网的元素个数有限性约束完全一致。另外,计划中的动作与有色网中的变迁语义类似,以及计划中的操作和状态和有色网中的库所语义非常类似。因此,有色网应用到计划的形式化中,有其独特的优势。本文根据约定的前提条件,计划建模从操作、状态和交互3个方面来具体实现,并给出了建模方法。计划的规范描述、有效性验证以及计划的模拟都可以直接应用经典Petri网或有色网的理论技术。 相似文献
18.
一种基于线性逻辑的时间Petri网推理方法 总被引:3,自引:0,他引:3
针对传统分析方法的不足 ,提出了时间 Petri网的线性逻辑表示和时间推理方法 .基于线性逻辑 ,定义了时间 Petri网中变迁之间的各种触发规则 ,在这些规则的基础上 ,提出了时间 Petri网运行行为的证明方法 ,此方法能清楚地分析时间 Petri网的运行行为和进行时间推理 . 相似文献