spin简介以及ispin运行样例

工具名称：iSpin 工具的适用范围和应用情况：此工具主要是用Promela编写实现。Promela是一种过程建模语言，其预期用途是验证并行系统的逻辑。给定Promela中的程序，Spin可以通过对建模系统的执行进行随机或迭代仿真来验证模型的正确性，或者可以生成C该程序对系统状态空间进行快速详尽的验证。验证程序还可以用于证明系统不变性的正确性，并且可以找到非进度执行周期。最后，它支持线性时间时间约

>>阅读原文<<