A Modeling and Verification Method of Modbus TCP/IP Protocol

With the informatization of industrial control system, industrial communication protocol is facing greater data pressure. At the same time, industrial communication protocols will face more security threats. In this paper, we use the method of transforming STM (State Transition Matrix) model to UPPAAL (a tool for verifying real-time system) model. In order to clearly understand the model and avoid some mistakes in the early stage of modeling, we first establish STM model for Modbus TCP/IP protocol. Finally, it is transformed into UPPAAL model. Five types of attributes are verified by UPPAAL tool, including the verification of unreachable attributes found by STM modeling. These five types of attributes verify the credibility of Modbus TCP/IP protocol. The experimental results show that this method can have a clear understanding of the model in the early stage. After converting STM model into UPPAAL model, more constraints can be found by referring to STM model. Compared with the existing methods, it studies the credibility of the protocol itself. Therefore, the method can find the root of the problem and solve it.