Petri网性质的线性时序逻辑描述与Spin检验

计算机科学 ›› 2006, Vol. 33 ›› Issue (5): 287-289.

Petri网性质的线性时序逻辑描述与Spin检验

段风琴李祥

贵州大学计算机软件与理论研究所,贵阳550025

出版日期:2018-11-17 发布日期:2018-11-17
基金资助:
贵州省科学基金项目（GGY2004002）.

DUAN Feng-Qin ,LI Xiang （Institute of Computer Seienee,Guizhou University,Guiyang 550025）

Online:2018-11-17 Published:2018-11-17

摘要/Abstract

摘要： Petri网是描述并发系统的很直观的图形工具Spin是一种著名的分析验证并发系统性质的工具。本文首先论述Petri网性质的线性时序逻辑描述，研究用Promela编程描述Petri网和用Spin对Petri网性质进行检验的方法，最后通过两个具体的示例说明这种方法是成功的。

关键词: 模型检测 Spin Promela Petri网线性时序逻辑

Abstract: Petri Net is an intuitional graphics tool of depicting subsequent system. Spin is a famous tool of analyzing and validating subsequent system. First this paper discusses the description of Petri Net＇s property using Linear TernT poral Logic. Then it inves

Key words: Model checking, Spin, Promela, Petri Nets, LTL

段风琴李祥. Petri网性质的线性时序逻辑描述与Spin检验[J]. 计算机科学, 2006, 33(5): 287-289. https://doi.org/

DUAN Feng-Qin ,LI Xiang （Institute of Computer Seienee,Guizhou University,Guiyang 550025）. [J]. Computer Science, 2006, 33(5): 287-289. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed