# Formal Safety Assessment and Improvement of DDS Protocol for Industrial Data Distribution Service
## 3 Related Foundation  
### Formal Modeling Methods Comparison  
Protocol engineering uses formal description technology to strictly design and maintain various activities of the protocol, and establishes an accurate protocol model to verify the logical correctness of the protocol. At present, the more popular formal methods for network protocols include state machines, temporal logic, Petri nets, etc., and these methods have their own characteristics.  
Protocol state machines, are finite state machines or automata that describe the message sequences that can occur as sessions for some protocol. Traditional state machines can adeptly model many constructs and extract and analyze their behavior. Unfortunately, state machines do not scale well due to state space explosion. In addition, the state machine is only suitable for describing small and simple protocols, and it is single-threaded, which has limited ability to describe the complex systems of many large-scale applications in the real world. When analyzing and verifying the state machine model, reachability analysis technology is usually used, which needs to manually generate a state reachable tree, which is prone to state space explosion and cannot prove the activity of the protocol. Therefore, simply using the state machine theory to model the multi-concurrent session system of the security protocol will not be effective.  
Temporal logic is an extension of modal logic. Temporal logic is mature in application and has strong mathematical abstraction ability. It focuses on describing the system by defining externally visible action events of the system, and does not care about the details of internal changes in the protocol. It is easy to describe the activity of the protocol, it is also easy to verify the protocol model. However, it is too abstract to describe the logical structure of the protocol.  
The Petri net model is based on the concept of concurrency, and the description system is simple and intuitive. At the same time, it has a complete analysis method and mature analysis tools, and is widely used in distributed software systems, parallel computing, network communication protocols and other fields. CPN adds a color set to classify tokens on the basis of traditional Petri nets, which requires the definition of variables and functions to realize the flow of different tokens on the arc, thereby improving the expressive ability of Petri nets and the ability to describe complex systems. CPN supports the hierarchical abstraction technology of models, which can model complex system behaviors at different levels of abstraction, and supports efficient model analysis and confirmation. CPN is a concurrent and typed enhancement of a state machine, with a mature modeling platform, and CPN Tools is a powerful modeling and analysis tool set for editing, simulating, and analyzing the state space of the CPN model. Combined with the programming language CPN Markup Language (ML), its ability to describe large and complex systems is greatly improved.  
Through comparative analysis, this paper believes that the CPN method has more advantages in describing network protocols. Although CPN is similar to a state machine, it is suitable for complex concurrent protocols due to its powerful and easy-to-understand state space analysis capabilities. The state space explosion is easier to manage, and DDS is a large and complex protocol, so we use CPN to simulate this agreement.