【摘要】 Petri 网是描述并发系统的很直观的图形工具;Spin 是一种著名的分析验证并发系统性质的工具。本文首先论述 Petri 网性质的线性时序逻辑描述,研究用 Promela 编程描述 Petri 网和用 Spin 对 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 Tem- poral Logic.Then it investigates that how to depict Petri Net using Promela and the way to validate the property of Pe- tri Net using Spin.At last this method is proved to be success through two idiographic examples.更多还原