ESpin:基于SPIN的Eclipse模型检测环境
信息化社会中人们对软件可信性的要求越来越高，传统的测试技术已经不能充分保证系统的安全性，基于模型的形式化验证技术成为解决此类问题的重要途径.SPIN作为典型的模型检测工具，在学术界和工业界都得到了广泛应用.本文在Eclipse平台上设计并实现了一个基于SPIN的易扩展的模型检测环境ESpin.环境通过一个优化了的代码分区算法和可迅速支持SPIN升级的文法分析器，构造了一个高效的、易扩充的Promela编辑器.编辑器除了支持Promela的全部语法规则外，还提供了包括实时语法反馈、关键字高亮、大纲视图、代码折叠、代码提示、代码补全在内的多种功能，提高了复杂模型的建模效率.此外，环境还为用户提供了多种运行模式和特有的向导、配置界面，简化了SPIN的操作过程.
软件验证 模型检测 SPIN Promela模型
吕威 黄志球 陈哲 阚双龙
南京航空航天大学 计算机科学与技术学院,南京市 中国 210016
国内会议
南京
中文
1-9
2012-10-20（万方平台首次上网日期，不代表论文的发表时间）