Modeling and reliability verification of industrial control network protocol based on time state transition matrix

With the improvement of industrial informatization, various industrial control system network protocols have also been widely used. The reliability of these protocols will directly affect the safety of industrial control systems. As an effective method that can automatically analyze system reliability, model checking has been widely used in the verification of various safety-critical systems. In this paper, we propose a modeling design method for industrial control network protocol based on time semantic reconstruction of time state transition matrix (TSTM). In addition, we provide a TSTM model checking method based on linear temporal logic (LTL). In order to effectively alleviate the state space explosion, the method adopts bounded model checking (BMC) technology. Furthermore, we implement a TSTM model verification tool called ICPV. Finally, we apply the above method to the modeling and verification of the industrial control network protocol Powerlink and through a comparison experiment with UPPAAL to illustrate the effectiveness of the method proposed in this paper.