Spin是Promela建模语言的解释器和验证工具。它本身有一个图形化的工具iSpin，不过这个图形化实在有些简陋。下面介绍一个Eclipse的插件，这样我们可以使用Eclipse的编辑环境来使用Spin。

首先，在Eclipse的install new software中添加 http://matrix.uni-mb.si/fileadmin/datoteke/znanost/orodja/ep4s/update-site/ 把Group items by category选项去掉，否则看不到可安装的插件；安装此插件。

然后，在菜单栏中选择Spin项，进入Spin Configuration，image

Spin工具可以从其官网下载。

C Complier里的gcc可以用cygwin安装，记得选择直接的版本，不要选择gcc.exe，否则可能出现不能验证通过的错误。

基本上这样就算安装完成了，如果你有什么问题，可以给我留言。