模型检测器SPIN图形化工具的研究与应用
Research and Application of the SPIN Model Checker Graphical Tools

作者: 陈平 , 王德成 :安徽新华学院,合肥;

关键词: 模型检测SPINPromelaLTLModel Checking SPIN Promela LTL

摘要:

模型检测是一种有着自动化并能提供反例的验证系统属性的形式化分析方法,其由系统模型,系统属性的描述和模型检测器组成。模型检测器接受模型和属性自动的去验证属性是否满足模型,如果不满足给出一个反例,其在软硬件验证中都得到了广泛的应用。模型检测器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.

文章引用: 陈平 , 王德成 (2014) 模型检测器SPIN图形化工具的研究与应用。 软件工程与应用, 3, 70-77. doi: 10.12677/SEA.2014.33009

参考文献

[1] Holzmann, G.J. (2003) The SPIN model checker: Primer and reference manual. Addison-Wesley, Bos-ton.

[2] Ben-Ari, M. (2008) Principles of the spin model checker. Springer Verlag, London.

[3] Spin Readme. http://spinroot.com/spin/Man/README.html

[4] Spin Sources. http://spinroot.com/spin/Src/index.html

[5] Spin verifier’s roadmap: Using iSpin. http://spinroot.com/spin/Man/GettingStarted.html

[6] Gerth, R., Peled, D., Vardi, M.Y. and Wolper, P. (1995) Simple on-the-fly automatic verification of linear temporal logic. Proceedings of the 15th International Conference on Protocol Specification, Testing and Verification, Warsaw, 3-18.

[7] Promela Manual Pages. http://spinroot.com/spin/Man/promela.html

[8] Boigelot, B. and Godefroid, P. (1996) Model checking in practice: An analysis of the ACCESS bus protocol using SPIN. 3rd International Symposium of Formal Methods Europe Co-Sponsored by IFIP WG 14.3 Oxford, 18-22 March 1996, 465-478.

[9] 孙守卿 (2006) 基于模型检测工具SPIN的安全协议分析和验证. 硕士学位论文, 兰州大学, 兰州.

[10] 刘俏威 (2008) SP州模型检测的形式化分析机理研究及应用. 硕士学位论文, 南昌大学, 南昌.

[11] Raynal, M. (1988) Distributed algorithms and protocols. JohnWiley & Sons, New York.

[12] 易锦, 张文辉 (2006) 从基于迁移的扩展Buhci自动机到Buchi自动机. 软件学报, 4, 720-728.

分享
Top