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

Analyzing Petri Nets'Property Using Spin

作　　者：段风琴[1] 李祥[1] 

机构地区：[1]贵州大学计算机软件与理论研究所,贵阳550025

出　　处：《计算机科学》2006年第5期287-289,共3页Computer Science

基　　金：贵州省科学基金项目(GGY2004002)

摘　　要：Petri 网是描述并发系统的很直观的图形工具;Spin 是一种著名的分析验证并发系统性质的工具。本文首先论述 Petri 网性质的线性时序逻辑描述,研究用 Promela 编程描述 Petri 网和用 Spin 对 Petri 网性质进行检验的方法,最后通过两个具体的示例说明这种方法是成功的。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 investigates that how to depict Petri Net using Promela and the way to validate the property of Petri Net using Spin. At last this method is proved to be success through two idiographic examples.

关 键 词：模型检测 SPIN PROMELA PETRI网 线性时序逻辑 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]