软件是否可信赖已成为一个国家的经济、国防等系统能否正常运转的关键因素之一，尤其在一些诸如核反应堆控制、航空航天以及铁路调度等安全悠关(safety—critical)领域更是如此。这类系统要求绝对安全可靠，不容半点疏漏，否则将导致灾难性后果。如1861年8月英国克莱顿隧道事故，就是由于协议的不完整性造成的，还有1996年6月4日，欧洲航天局阿丽亚娜(Ari—ane)501火箭因为其控制软件的规范和设计错误而导致发射37秒后爆炸。类似的报道屡见不鲜，如何确保这些系统的可靠性成为计算机科学与控制论领域共同关注的一个焦点问题。 据统计，在美国每年要花去3000亿美金用来雇佣程序员专门来解决程序的BUG，而这个工作就占据了整个产品开发周期40％～60％的时间。尽管花费了这么大量的人力和物力来排除BUG，他们还是不能保证软件没有错误。 为了从根本上保证软件系统的可靠安全，包括图灵奖得主A．PnDeli在内的许多计算机科学家都认为，采用形式化方法(formalmethds)对系统进行形式化验证和分析，是构造可靠安全软件的一个重要途径。模型检测技术是形式验证方法中的一种。而获得ACM(Association for Computing Machinery)软件系统奖(Software Systems Award)的SPIN就是著名的模型检测工具之一。 典型的SPIN工作模式是首先对并发式系统或分布式算法的规范建立高标准的模型，在确认没有语法错误后，对系统的交互进行模拟，直到确认系统设计拥有预期的行为，然后SPIN产生一个用C语言描述的验证程序，经检验机编译后被执行，执行中如果发现了违背正确性说明的任何反例，则反馈给交互模拟机，通过重现细节剔除引起错误的原因。 本文首先详细介绍了著名的模型检测工具SPIN的历史、发展与特点，讨论了使用SPIN对网络通信协议分析的方法。本文所做的主要工作、技术难点与创新处如下： ● SPIN(Simple Promela Interpreter)是适合于并行系统，尤其是协议一致性的辅助分析验证工具，本文讨论了在Win32下和Cygwin／Linux／Unix下对SPIN的安装和使用。 ● 使用SPIN的最简单的方式是使用图形界面XSPIN，图形界面独立于SPIN运行，辅助产生和选择相应的SPIN命令，XSPIN在后台运行SPIN得到期望的输出值，XSPIN知道什么时候怎么样去编译模型检测的代码，也知道什么时候如何去执行它，所以可以不用记住所有的参数。本文介绍了在Cygwin下安装和使用SPIN的图形界面工具XSPIN。 ● Promela(Protocol／Process Meta Language)是用来对有限状态系统进行建模的形式描述语言，本文阐述了如何使用Promela语言对协议进行描述。 ● AB协议是最早的端到端的通信协议之一，用SPIN对AB协议进行分析从而得到协议中不容易发现的错误。 ● 使用SPIN的图形界面XSPIN对上述协议进行分析得到直观的进程之间信息的交互图。 ● SPIN不仅可以用来验证协议的正确性，也可以对身份验证协议进行有效的攻击检测。本文讨论了在网络保密通信中使用密钥分配中心KDC系统时的攻击问题，用Promela语言建立了KDC的模型，使用LTL描述其性质，用SPIN进行模型检测验证，使用XSPIN得到协议受攻击的轨迹图形。 ● 对NSSK协议进行建模和分析，得到协议受攻击的轨迹。对Woo_Lam协议进行建模和分析，得到协议中潜在的两个受攻击轨迹。