实验报告实验题目：基于SPIN的LTL模型检测课 程 名： 形式化方法 姓 名： 王燕霞 学 号： 201428013229141 一、SPIN概述SPIN是由贝尔实验室形式化方法与验证小组用ANSI C开发，可以在所有UNIX操作系统版本使用，也可以在安装了Linux、Windows95以上版本等操作系统中使用，适合于分布式并发系统，尤其是协议一致性的辅助分析检测工具。 SPIN模型检验工具的基本思想是求两种自动机所接受语言的交集，若交集为空集，则安全特性得到验证，否则输出不满足安全特性的行为迹。SPIN可以用于以下三种基础模型中：1）作为一个模拟器，允许快速对建立的系统模型进行随意的、引导性的或交互的仿真。2）可以作为一个详尽的分析器，严格的证明用户提出的正确性要求是否满足（使用偏序简约进行最优化检索）。3）用于大型系统近似性证明，用SPIN可以对大型的协议系统进行有效的正确性分析，即使这个系统覆盖了最大限度的状态空间。二、SPIN的
