摘要： 本文针对一种最新提出的卫星网络管理协议，利用Petri网描述协议的方法，对此网络管理协议过程进行了形式描述，利用Petri网的可达树、不变量对协议的有界性、活性、守恒性、完整性、前进性等性质进行了验证，确定了协议的逻辑正确性，在此基础上，完成了此协议的实现并对其性能进行了测试。

关键词: Petri网 网络管理协议 验证 形式描述 性能测试 正确性 完整性 卫星网络 可达树 不变量