WAP事务协议(WTP)作为WAP协议体系结构中的一个重要部分,向会话层提供基于请求响应的分布式事务服务。由于WAP论坛将WAP协议规范以自然语言的形式发布,这样的好处是可读性好,便于直观上去理解。但是,要保证协议实现的一致、完整和正确就必须使用一种形式化的工具进行描述和验证,这样才能避免自然语言的二义性导致实现上的不一致。本文基于模型检测工具SPIN,对WTP事务层协议做形式化地分析和验证。首先对此协议从行为属性和安全性两方面进行抽象。包括对协议主体建立状态和状态转移描述;然后对协议采用PROMELA语言建立模型。协议的安全属性描述采用LTL逻辑公式。其次运用SPIN对协议的模型进行行为模拟,对LTL描述的协议属性进行正确性及安全性验证。在验证和模拟的过程中,随时根据模型的状态数目和系统的消耗调整抽象模型的结构和行为。对协议中不满足属性的验证结果进行分析和改进。最后,将分析和验证结果和其他安全协议的验证方法比较,总结现有工作和尚需完善的工作。