协议工程就是一体化、形式化的协议开发过程。协议工程的目的是用来减少协议开发中潜在的错误，提高协议开发的效率，促进标准化的发展。协议的形式化理论是协议工程的核心。它运用形式化方法进行协议工程学的研究，研究内容包括：协议分析、协议设计、协议描述、协议验证、协议实现和协议测试的理论和方法。协议形式化描述是协议实现和协议测试的重要前提，协议验证保证协议设计的正确性和完整性，协议测试是保证协议实现满足协议规范的重要手段。 本文以协议工程的理论为依据，并以AB协议为研究对象，首先从协议分析开始，研究了协议分析技术，并且对协议的上层用户及底层用户的环境要求进行了讨论分析；然后根据有限状态机的理论基础，研究了AB协议的有限状态机模型，并根据该模型通过SDL技术实现了对协议的描述和仿真；最后，进一步研究了协议验证的相关概念，本文讨论了几种验证方法，并对其中的一种方法提出改进，在此基础上采用改进的方法对AB协议的状态机模型进行了验证。通过验证结果的对比，显示了改进方法的优越性。