模型检测器SPIN图形化工具的研究与应用

摘要

模型检测是一种有着自动化并能提供反例的验证系统属性的形式化分析方法,其由系统模型,系统属性的描述和模型检测器组成。模型检测器接受模型和属性自动的去验证属性是否满足模型,如果不满足给出一个反例,其在软硬件验证中都得到了广泛的应用。模型检测器SPIN是由贝尔实验室开发的一种适合于并发系统的模型检测工具。本文在介绍了SPIN的设计和结构,分析了其理论基础,并通过具体例子阐述了安装和使用模型检测器SPIN和它的图形化界面iSpin的使用方法。SPIN接受Promela语言建立的模型和使用线性时序逻辑LTL描述的性质,给出验证结果。本文在研究模型检测工具SPIN的结构和原理的基础上,详细的阐述了其图形化界面iSpin的安装和使用。