网络协议辅助设计系统中可达性分析的设计与实现

摘要

在网络协议的设计过程中,一个重要的段就是对协议的运行行为进行验证,以确定协议的正确性。本文采用可达性分析的方法,实现了对用Petri网描述的协议模型运行行为的自动验证,包括死锁验证、非法循环验证及特定状态的验证。