协议是网络的血液和生命，计算机网络的发展是网络协议设计和开发的结果。随着通信网络向着高速度、高性能、多媒体等方向的发展，协议变得越来越复杂，通信协议的设计已经成为通信网络设计和实现的关键。 本文首先介绍协议工程和基本的形式化模型。这些模型包括：有限状态机、扩展有限状态机、Petri网、进程代数、时态逻辑和抽象数据类型。它们是协议工程的理论基础和核心技术。 然后对形式化描述语言的三个国际标准(SDL、ESTELLE、LOTOS)进行了深入分析。指出了这三种形式化描述语言在描述协议模型方面的不足：它们都只能支持协议工程活动的某几个环节。统一建模语言LJML支持软件工程中从需求分析到设计实现部署的各个阶段。所以，uML在协议工程中的应用已经成为国内外一个研究热点。UML语言可能是一种更为理想的协议形式化描述语言。 最后深入研究了模型驱动构架MDA、UML及其建模技术，重点是UML类图和状态图。但是UML在描述状态机的行为时，缺乏清晰和严格的行为语义，导致不能直接用它来开发复杂协议。因此必须给UML增加行为语义。标准的形式化描述语言均提供了严格准确完备的行为语义。所以，如何将UML和标准的形式化描述语言融合起来是研究重点。 本文的创造性工作主要如下： ①提出UML状态图的交互抽象状态机模型IASMs。并用IASMs定义了一种具有消息传送功能的LJML状态图的形式化语义。 ②研究基于MDA的协议建模技术。利用LIML Profile机制，定义了一种“基于MDA的协议建模语言”——交互抽象状态机描述语言IASMsDL。基于MDA的PIM/PSM思想，开发了一个UML模型信息提取器R2TSPDL，定义了从UML模型到SDL模型的变换规则。 本文的研究成果己应用于导师承担的浙江省重点科技攻关项目“通信协议一致性测试集自动生成软件”之中，用于对被测协议的形式化建模并提取出后续用于协议一致性测试的模型信息。该项目是研究基于模型驱动构架的协议一致性测试集的自动生成。