随着互联网和分布式系统的广泛应用,电子商务的发展越来越迅速,相应的网络电子商务协议成为这种交易模式顺利进行的保证。电子商务协议的设计是一项非常庞大和复杂的工作,设计过程中极易出现意想不到的各种漏洞与缺陷,且协议在网络中呈现空间分布性、异步性和并发性等特征,这些都可能会导致不可估计的损失,因此对电子商务协议的分析与检测就成为一个现实的课题。形式化方法是分析验证电子商务协议的一种重要方法。传统的非形式化方法很难发现协议存在的潜在问题,于是形式化分析方法就成了研究的热点。目前有许多比较著名的形式化方法如BAN逻辑、串空间模型理论、定理证明等。而模型检测方法作为形式化分析方法中的一种,能够自动验证一个系统是否满足其设计规范,具有高度自动化和提供反例等优点,可以有效减少协议设计错误,近年来被广泛应用于软硬件验证中。SPIN是其中一种著名的用于分布式系统形式化验证的模型检测工具。本文基于模型检测工具SPIN,对HDPolyService系统中的一系列电子商务协议进行形式化分析和正确性验证。在阐述SPIN模型检测形式化分析验证机理、其建模语言PROMELA基本语法及线性时序逻辑LTL性质的基础上,详细介绍这三种“分布式”事务协议,通过分析协议设计规范提取出协议的形式化描述与状态行为转移关系,并转化为PROMELA模型作为SPIN检测工具的输入；然后根据协议模拟结果对模型进行修改完善,并采用线性时序逻辑LTL刻画出协议期望满足的属性,使用SPIN进一步检测是否满足该属性；最后根据分析和验证结果对协议设计进行完善,并总结当前工作和展望后续研究计划。验证结果表明应用SPIN对电子商务协议分析检验的可行性与普遍适用性,同时表明了这三种协议的实际应用价值。