Modeling and Verifying OPC UA of Aggregating Server Architecture for Vertical Integration

With the development of Industry 4.0 (I4.0), the demand for a protocol to unify communication between different devices is dramatically increasing. OPC Unified Architecture (OPC UA) is a protocol that can be used to accomplish information interoperability in manufacturing and its usage is expanding. Some research has been conducted on the implementation approaches for aggregating server pattern OPC UA in vertical integration. However, few efforts have been made on the formal verification of OPC UA as a vertical communication protocol to facilitate manufacture. In this paper, we design an aircraft parts production use case where vertical communication between the management layer and shop floor devices is achieved via OPC UA aggregating server architecture. Information Model and Services are two fundamental contents of the OPC UA protocol. With the help of process algebra Communicating Sequential Processes (CSP), we build the use case OPC UA model and realize both the Information Model and Services using a verification tool, Process Algebra Toolkit (PAT). We verify the general properties of the system (Divergence Freedom and Deadlock Freedom) and functional properties of OPC UA (Service Read Success, Service Call Success, Monitor Variable Success and Monitor Event Success). The results demonstrate the feasibility of the OPC UA protocol in vertical communication.