大部分网络协议具有分布式特征,需要由分布在网络设备中的协议实现共同协作完成一定的协议功能。协议互操作性测试是保证位于不同网络设备上的协议实现之间正确互连和协作的重要手段,其主要目标是测试多个协议实现是否能够正确的交互工作,从而完成协议标准中规定的功能。本文采用形式化技术,对分布式协议互操作性测试进行了深入研究,主要的研究内容和结论包括:对协议互操作性测试及分布式协议测试的研究现状进行了综述,指出当前研究中只考虑了一对一的简单情况,而对一对多等更为普遍的情形研究甚少。本文提出了一种互操作性测试理论框架,该框架适用于一对多等更为普遍的情形。首先定义了被测系统的抽象模型,引入互操作性关系的抽象概念,并给出了互操作性测试各阶段的形式化定义。为描述协议的输入输出行为,将系统模型为通讯多端口有限状态机CMpFSM;对于具有时间约束的协议,进一步采用通讯多端口时间输入输出自动机CMpTIOA作为系统模型;针对上述两种模型,分别明确给出互操作性关系的具体含义,作为互操作性测试的测试依据。提出了一种采用多个测试器的分布式协议互操作性测试生成方法。首先根据系统的CMpFSM模型生成全局测试序列,并进一步提出了一个增强的测试生成算法得到具有更高错误覆盖度的测试集;然后根据选定的分布式测试架构,将全局测试序列分布到各测试器上,最终生成分布式同步测试序列。时间约束是协议的重要功能,本文基于CMpTIOA模型研究了具有时间约束的协议互操作性测试。提出了一种基于时间互操作性关系的互操作性测试生成方法,该方法集成了可执行性预判决机制,最终生成参数化测试行为树,在一定程度上缓解了状态爆炸问题。进而研究了两种实时测试集描述法——实时TTCN和TIMEDTTCN-3,提出了从测试行为树到测试集描述法的转换方法,对于不能完全满足描述需求的测试集描述法实时TTCN,提出了一种扩展方案。设计和实现了基于上述两种实时测试集描述法的测试执行子系统,构造了测试系统原型。本文提出的理论和方法已在下一代互联网协议IPv6的互操作性测试中得到了应用。