摘要
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.
出处
《计算机科学》
CSCD
北大核心
2006年第5期287-289,共3页
Computer Science
基金
贵州省科学基金项目(GGY2004002)
