Abstract: The demand of software reliability has been greatly increased in today’s information society. Model-based formal verification has become a significant method to ensure the safety of software systems, while traditional techniques like software testing can no longer guarantee that. As a typical toolkit of model checking, SPIN（Simple?Promela?Interpreter） has been widely used in both academia and industry. This paper documents the design and implementation of ESpin, a highly-extensible SPIN-based model checking environment upon Eclipse. ESpin is an efficient and scalable editor of Promela, with an optimized code-partitioning algorithm and an upgradable grammar analyzer of SPIN. The editor has full support of the syntax rules of Promela, and also provides the function of real-time syntax feedback, keywords highlight, outline view, code folding, hinting and completion, greatly improving the modeling efficiency of complex models. Additionally, ESpin provides multiple operation mode and unique configuration interfaces, which simplifies the operation process of SPIN.

Key words: soft verification, model checking, Simple Promela Interpreter（SPIN）, Promela model

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

关键词: 软件验证, 模型检测, 简单进程元语言解释器（SPIN）, Promela模型