| ESpin*：基于SPIN的Eclipse模型检测环境 |
| |
| 引用本文： | 吕 威,黄志球,陈 哲,阚双龙,魏 欧.ESpin*：基于SPIN的Eclipse模型检测环境[J].计算机工程与应用,2013,49(7):45-51. |
| |
| 作者姓名： | 吕 威 黄志球 陈 哲 阚双龙 魏 欧 |
| |
| 作者单位： | 南京航空航天大学 计算机科学与技术学院，南京 210016 |
| |
| 摘 要： | 信息化社会中人们对软件可信性的要求越来越高，传统的测试技术已经不能充分保证系统的安全性，基于模型的形式化验证技术成为解决此类问题的重要途径。SPIN作为典型的模型检测工具，在学术界和工业界都得到了广泛应用。在Eclipse平台上设计并实现了一个基于SPIN的易扩展的模型检测环境ESpin，通过一个优化了的代码分区算法和可迅速支持SPIN升级的文法分析器，构造了一个高效、易扩充的Promela编辑器。编辑器除了支持Promela的全部语法规则外，还提供了包括实时语法反馈、关键字高亮、大纲视图、代码折叠、代码提示、代码补全在内的多种功能，提高了复杂模型的建模效率。ESpin还为用户提供了多种运行模式和特有的向导、配置界面，简化了SPIN的操作过程。
|
| 关 键 词： | 软件验证 模型检测 简单进程元语言解释器（SPIN） Promela模型 |
|
| 点击此处可从《计算机工程与应用》浏览原始摘要信息 |
|
点击此处可从《计算机工程与应用》下载全文 |
|
