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

• 作者: 王德成 陈平
• 来源期刊: 软件工程与应用
• 学科: 工学
• 关键词: 模型检测 SPIN PROMELA LTL
• 年，卷（期）: 2014,（3）
• 页码范围: 70-77
• 页数: 8页
• 分类号: TP39

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王德成		15	7	2.0	2.0
2	陈平		5	4	1.0	2.0