SDH协议在现代信息传输中显露出了强大的生命力.SDH收/发器是用于SDH光网络的重要器件,是SDH的协议实现.为了对SDH协议进行更彻底、更正确、更全面的测试,本文将在对SDH形式化模型进行正确性验证的基础上,利用开发的测试系统工具对逻辑仿真的SDH收/发器进行测试,最终完成对SDH协议的测试工作.形式化模型采用了直观高效的EFSM模型和Petri网模型,并以这两种模型为例,提出了基于模型转换的正确性验证方法,对SDH形式化模型进行了验证,随后依据一致性测试理论,本文提供了采用UIO方法生成SDH测试序列的途径,并为补充测试序列完备性增加了相应的测试用例.利用TCL/TK开发的SDH测试系统采用管道-过滤器技术设计,并使用缓冲区管理机制对管道进行了扩展;同时系统平台还提供了TCL扩展接口,测试者可以通过测控软件的人机交互接口直接对SDH测试过程进行动态控制.对SDH协议进行形式化建模,是贯穿此项协议工程始末的核心技术,对SDH形式化模型进行正确性验证,是进行协议测试的保障,我们开发的SDH测试系统,又为SDH这种新型的传输机制提供了一个有效的测试工具.基于正确性验证的SDH协议测试,从理论的高度为协议测试拓展了一条新颖的思路,而后续开展的测试实践又直观地展示了此项研究最终能达到的效果.本文主要完成了利用EFSM模型以及Petri网模型为SDH协议进行形式化建模的示例;随后研究模型间相互转换的理论,提出了基于模型互换的正确性验证方法,并利用此法对SDH的形式化描述进行了验证;在正确性验证的保证下,分析SDH协议一致性测试中不完备的部分,针对发现的协议错误补充测试用例,生成更完备测试序列集合;最终利用开发的SDH测试系统工具,对SDH的被测实现进行测试并分析了测试结果.