A formal model of satellite communication system network control protocol based on generalized stochastic Petri nets

Satellite network control protocol plays an important part in satellite communication systems. Any bug in protocol design and development phase will cause great losses or damages. To avoid the potential errors, the formal method Petri nets is applied to describe the satellite network control signaling protocol and verify some critical properties of protocol. The paper focuses on interaction behaviors in signaling protocol and abstracts basic patterns from protocol. Then, it provides a generalized stochastic Petri nets based signaling protocol model. By means of the formal model, the protocol reliability and performance are evaluated through interaction behavior analysis, structure analysis and quantitative analysis.