Abstract: An abstract principle is proposed to mitigate the explosion of state space.The proposed scheme scientifically reduces the auxiliary variables, message fields and numbers of automatic state machines in the process of model design, and reduces the complexity and size of the model on the premise of minimizing the accuracy of verification results.A semi-automatic modeling framework is proposed thereafter, which can automatically generate models with uniform specifications with only a small amount of input provided by users and no need to learn grammar, which is convenient for researchers to consult and use.Experiments show that the model based on the proposed abstract principle and the semi-automatic modeling framework can verify the properties of the network protocol.

Key words: model detection, network protocol, abstract principle