ESpin??:基于 SPIN 的 Eclipse模型检测环境

摘要：

信息化社会中人们对软件可信性的要求越来越高,传统的测试技术已经不能充分保证系统的安全性,基于模型的形式化验证技术成为解决此类问题的重要途径.SPIN 作为典型的模型检测工具,在学术界和工业界都得到了广泛应用.在 Eclipse 平台上设计并实现了一个基于 SPIN 的易扩展的模型检测环境 ESpin,通过一个优化了的代码分区算法和可迅速支持 SPIN 升级的文法分析器,构造了一个高效、易扩充的 Promela 编辑器.编辑器除了支持 Promela 的全部语法规则外,还提供了包括实时语法反馈、关键字高亮、大纲视图、代码折叠、代码提示、代码补全在内的多种功能,提高了复杂模型的建模效率.ESpin 还为用户提供了多种运行模式和特有的向导、配置界面,简化了 SPIN 的操作过程.

关键词：软件验证、模型检测、简单进程元语言解释器(SPIN)、Promela模型

分类号：TP306(计算技术、计算机技术)

在线出版日期：2013-04-28（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：45-51