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

Research and Application of the SPIN Model Checker Graphical Tools

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

Abstract: Model checking is an automated formal analysis method which can provide counter-examples to verify system properties. It consists of system model, system described attributes and model checker. Model checker accepts model and attributes to verify whether the property meets the model automatically. If it is not satisfied, a counter-example will be given. Hardware and software verification have been widely used. SPIN model checker has been developed by Bell Labs, which is suitable for concurrent systems model checking tools. This paper describes the design and structure of SPIN, analyzes the theoretical basis and elaborates the installation & use of SPIN model checker and its graphical interface, iSpin, by specific examples. SPIN Promela language accepts the model established by the Promela language and the nature described by using linear temporal logic (LTL); hence, the results are verified. Based on the study of SPIN’s structure and principle, a detailed exposition of the installation and use of its graphical interface iSpin is given.