Modeling and Verifying OPC UA Protocol for Vertical Integration

With the advancement of Industry 4.0, the deep integration between industrial production and information technology continues to evolve, leading to a rapidly growing demand for a unified communication protocol to transfer data across heterogeneous devices and hierarchical levels in manufacturing systems. In this context, the Open Platform Communications Unified Architecture (OPC UA) is developed to eliminate communication barriers between different devices in manufacturing environments. As the adoption of OPC UA in industrial applications is spreading, research focusing on its implementation in production control systems continues to expand. Researchers are actively exploring using OPC UA in cross-layer vertical integration to reduce inter-layer communication costs for industrial production control. This paper seeks to establish a theoretical foundation for the application of OPC UA in vertical integration by employing formal methods to rigorously verify its security guarantees and operational viability. This paper presents the first comprehensive formal verification of OPC UA for cross-layer vertical integration. By utilizing the formal modeling language Communicating Sequential Processes (CSP), we develop the model of OPC UA vertical integration across several industrial layers. The model captures two core procedures: communication establishment and production control. In communication establishment, the cryptographic key exchange mechanism between Manufacturing Execution System (MES) and Workshop via OPC UA protocol is formally modeled, with intrusion scenarios incorporated to systematically evaluate protocol security. In production control procedure, vertical integration spanning MES, aggregation servers in Workshop layer, and devices in shop floor layer is rigorously analyzed and validated, using a unified OPC UA information model. Through the Process Analysis Toolkit (PAT), we implement and verify the model. The results demonstrate that the system satisfies deadlock-freedom, divergence-freedom, data reachability, and data security under attack. For a production control scenario with 5 devices, the verification of all properties completed in under 2 min, demonstrating the feasibility of our approach for systems of nontrivial scale. These results provide a formal foundation for the secure and reliable application of OPC UA in Industry 4.0 manufacturing systems, moving beyond testing-based validation to offer mathematical guarantees of correctness and security for vertical integration.