论文部分内容阅读
协议的规格说明主要是以自然语言描述的,对其进行形式化的目的是精确描述协议,减少开发人员对协议规格说明理解的偏差,B方法以数学理论为基础,可产生简明、精确、无歧义且可证明的规格说明,B方法的优点使得它适合对协议进行形式化描述和一致性测试。本文详细介绍了使用B方法对TCP状态非典型变迁进行形式化,并据此生成了测试用例,提高了TCP协议一致性测试的质量和可靠性。