网络协议的形式化分析与设计

随着形式化方法和技术的日趋完善,网络协议的开发已逐步从非形式化描述、手工方法实现过渡到已形式化描述技术为基础,渗透到网络协议分析、综合、测试等各环节的软件工程方法。本文从网络协议的基本要素、协议的形式化模型介绍了网络协议,并从协议的性质描述、不变性分析、可达性分析、基于有序二叉判决图的符号模型检验对网络协议进行了形式化设计与验证,最后进行了测试。