随着通信行业的蓬勃发展,服务于各个层面的通信协议也被制定出来。对通信软件的要求也越来越高。但在通信软件开发方法中,面临着诸多问题。诸如:协议实现和协议描述的不一致性;编程人员编写错误;测试不充分等。采用形式化方法对信息处理系统进行描述,有效地保证协议实现与协议规范的一致性。协议测试集自动生成方法有效地简化了协议测试的工作,缩短了协议的开发时间。而采用由SDL描述的系统自动生成可执行代码,也可以有效地避免编程的错误。论文以IMS的MGCF开发为背景,通过以“形式化的方法”开发其上的协议软件,探索形式化工具在开发协议软件的建模、仿真、代码生成和代码测试的各环节的解决方案。论文首先回顾了当前主要的形式化描述方法与测试集自动生成技术。然后进行了分析和研究。总结出SDL与C混编,自动测试技术与人工测试并用的通信软件开发模式。最后采用该开发模式开发了MGCF的部分功能模块,为相关的开发提供了有益的经验。