关键词: 多元化网络管理协议, Petri网, 可达性分析, S-不变量分析, T-不变量分析

Abstract: Introduces a new management protocol into satellite network, of which the design of service connection/primitives is explained. The way to describe a protocol with Petri net is applied to giving a formal description of the protocol model. Moreover, the analyses of the reachability, S_invariants and T_invariants of Petri nets are utilized to verify the logical correctness of the protocol, thus making sure its boundedness, liveliness, conservation, completeness arid advancement, reducing potential mistakes in protocol designing and laying well a foundation to implement the protocol.