论文部分内容阅读
本文对通信协议形式化描述和验证理论与方法进行了研究。文章在用Petri网模型对通信协议进行形式化描述的基础上提出了用Petri网展开图对通信协议进行验证，从而提出了一种新的通信协议形式化验证方法。文章主要内容包括：对各种形式化描述语言和模型进行了综述，重点分析了Petri网对通信协议的描述能力；对各种形式化验证方法进行介绍和分析；对Petri网描述模型的验证性进行了分析，特别分析了Petri网的展开图方法在验证Petri网行为属性方面的应用；使用Petri网模型对两种典型的通信协议(TFTP协议和BGP协议)进行形式化描述；在此基础上，使用Petri网展开图方法对两个协议的行为属性进行了分析，并且通过对植入错误的协议描述的分析证明了展开图法具有一定的纠错能力。