TOP状态非典型变迁的形式化研究

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