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.

The rapid development of the Internet of Things (IoT) spurs strong global demand for related applications and technologies, especially in enhancing system reliability and security. Communication security, mobility, and real-time are the three vital features for constructing secure and reliable IoT systems. Formal methods, based on rigorous mathematical theory, are widely used to describe, analyze, model, and verify software and hardware systems, significantly improving their security and reliability. However, the current research mainly focuses on the practical applications of IoT, and there are still few studies on applying formal methods to IoT systems. As a response, our recent work has proposed the SMrCaIT calculus, which is the only process calculus currently designed for IoT that can comprehensively describe the security, real-time, and mobile features of IoT. Applying the SMrCaIT calculus enables us to model and verify IoT systems before their actual implementation, thereby providing a solid theoretical foundation for building secure and reliable IoT systems. To verify the correctness of the SMrCaIT programs, this article presents a proof system for SMrCaIT calculus, based on the extended Hoare Logic considering time. Additionally, we explore the cooperation test between isolated proofs to further ensure that messages are delivered correctly between IoT entities. The soundness of the proof system is also confirmed. A Vehicle Ad Hoc Network case and a Multi-Unmanned Aerial Vehicle case demonstrate the usability of our proof system in analyzing IoT scenarios.

The integration of formal modeling and data-driven analysis is crucial for addressing complex challenges in Manufacturing Operations Management (MOM) systems under Industry 4.0. While our previously proposed refinement calculus of Object-Oriented Event-Graph (rCOE) offered a preliminary syntactic and semantic foundation for MOM modeling, its operational semantics were only briefly outlined. This paper extends our prior work by providing a complete and rigorous formal definition of rCOE's operational semantics, enabling precise executable specification and dynamic analysis. Furthermore, using a synthetic yet industrially realistic dataset, we apply the Isolation Forest algorithm to identify key high-risk processes-such as "Matching Drill" with excessively long duration and near-zero pass rate, and "Straightening" with high execution frequency-that threaten production efficiency and product quality. To demonstrate the practical synergy between data-driven discovery and formal modeling, we model these critical processes using rCOE and conduct a simulation based on the operational semantics. The simulation successfully replicates the possible resource contention and scheduling conflicts, validating its ability to replicate anomalies and evaluate mitigation strategies. This work establishes an integrated, empirically-grounded formal methodology for enhancing the robustness of MOM systems, moving from anomaly detection toward explainable diagnosis and mitigative analysis.

The formal verification of IoT security protocols is often split into two largely independent domains. Qualitative analysis establishes logical correctness against active intruders, whereas quantitative analysis evaluates performance metrics such as latency and energy consumption. Maintaining separate models for these purposes is both labor-intensive and prone to semantic drift, leading to a recurring mismatch: protocols that appear secure in theory may fail once exposed to stochastic constraints of real-world networks. To address this gap, we propose a unified framework anchored by Pat2Prism, a novel tool that automates the translation of CSP-based specifications into probabilistic models. Beyond mere automation, we establish a rigorous theoretical foundation for this transformation. We define a formal mapping from Process Analysis Toolkit (PAT)’s Labeled Transition Systems (LTSs) to PRISM’s Markov Decision Processes (MDPs) and prove that it preserves trace semantics and safety properties, ensuring quantitative insights are drawn from a behaviorally faithful refinement of the verified specification. We evaluate the framework on the CoAP-EAP protocol and its lightweight variant, Lo-CoAP-EAP. Although both pass qualitative verification, quantitative results expose a critical trade-off: the 7.87

Thread is an important mesh networking technology that enables reliable and secure communication among Internet of Things (IoT) devices. At the core of Thread, the Mesh Commissioning Protocol (MeshCoP) authenticates and securely joins new devices. However, the complexity of MeshCoP which arises from cryptographic handshakes among multiple participants poses challenges for the verification. Existing approaches based on the overall models often suffer from state space explosion and limited scalability, making it difficult to analyze both local and global cross phase properties in a tractable way. To address these challenges, we propose a decoupled and automata-based approach for the formal verification of MeshCoP. The commissioning process of MeshCoP is decomposed into four individual phases, and each phase is modeled as a network of timed automata in UPPAAL. Then, the four decoupled models are independently verified to ensure internal correctness, effectively reducing complexity. Subsequently, inspired by the Assume-Guarantee method, we further abstract these submodels based on the verified properties, omitting the details of the interactions and preserving local correctness. Finally, we integrate them into a unified system and verify the cross phase properties of MeshCoP. The results demonstrate that the decoupled approach can provide a reusable and extensible framework for analyzing complex protocols.

Modern hardware architectures and mainstream programming languages employ relaxed memory models for efficiency purposes. However, these memory models may bring in many behaviors which do not adhere to people’s intuition. In addition, different relaxed memory models produce different relaxed behaviors. The existing facts make the verification of the multi-threaded programs running against these models more difficult. In this paper, we are committed to proposing a general framework for modeling and verifying programs over various relaxed memory models, and we take the MCA ARMv8 architecture as an example. This architecture allows out-of-order execution through thread-local out-of-order, speculative execution and thread-local buffering. Above all, through analyzing the dependencies among statements, any program under MCA ARMv8 is translated into a unified form, which has the ability to describe each program under various memory models. Then, we model the translated programs with the formal specification language TLA[Formula: see text], and verify three properties, namely Reordering, Read-after-write elimination and Barriers, by the model checker TLC. Our verification results indicate that these properties align with the specification of MCA ARMv8. This not only validates the effectiveness of our method but also provides a more consistent approach for ensuring program correctness across a wide range of memory models.

Modeling and verification of multithreaded programs are difficult since one must consider all the ways that instructions in different threads can be interleaved. Modern hardware architectures and mainstream programming languages employ weak memory models (WMMs) for efficiency reasons, and the additional interleavings from them make the modeling and verification more complex. In addition, different WMMs cause various relaxed-memory effects, and their operational semantics has distinguished expressions and transition rules. On this basis, multiple algorithms are required to be designed to conduct verification on programs over WMMs. In this paper, we propose a lightweight modeling and verification framework for programs over WMMs. Above all, we apply Unifying Theories of Programming (UTP) to investigate the unified algebraic semantics. A set of algebraic laws are explored, which can dynamically generate configuration sequences of programs under WMMs. Two memory models, total store order (TSO) implemented in the 86 architecture and SPARC implementations, and ARMv8 supported by the ARM architecture, are used to instantiate the proposed algebraic modeling method. During this process, we record the data state of each configuration and define properties capturing the unique features of the TSO and ARMv8 memory models, and then check whether the properties are satisfied. The algebraic laws are implemented in the rewriting engine Maude, and the verification is also conducted in Maude. The verification results show that the properties all agree with our expectations.

Relational Hoare logic [18] extends the applicability of modular deductive verification to encompass the verification of crucial 2-run properties, such as confidentiality. Most of the current research on relational Hoare logic primarily focuses on its practical applications. However, incorporating parallel programs into the logic may further complicate the system design, which is an aspect that most research has overlooked. Therefore, this paper updates the previous system, referred to as the relational system, by incorporating parallel composition. Based on the Unifying Theories of Programming (UTP), we further explore the denotational semantics and algebraic semantics of the system with 2-runs, employing relational denotational and algebraic semantics for representation. And the study of the conditional construct and parallel composition are the crucial points. To facilitate the algebraic exploration of parallel expansion laws, we extend the system with a new concept called guarded choice, enabling the transformation of any program into a guarded choice form.

The Business Process Model and Notation (BPMN) has become a widely accepted standard for business process modeling. However, much of the formal verification research on BPMN is based on earlier versions and often overlooks unstructured and loop elements. This paper presents a novel approach to BPMN verification using Hoare logic. In this paper, we enhance the expressiveness and precision of BPMN by explicitly incorporating conditions into decision gateways and loop tasks. Based on this enhancement, we provide formal semantics and dynamic state explanations for BPMN diagrams. A framework is designed to partition BPMN diagrams and verify properties with our proof system based on Hoare logic, offering an intuitive, state-space explosion-free method. A logistics case study demonstrates the framework’s applicability and effectiveness.

FastDFS is a lightweight distributed file system that fully incorporates redundant backup, load balancing, linear expansion and other mechanisms. It is easy to build a high-performance file server cluster using FastDFS. Given the widespread usage of FastDFS, carrying out its analysis within a formal framework is highly significant. In this paper, we first model and analyze FastDFS using process algebra CSP. The three key functions that we concentrate on are uploading, downloading, and deleting files. Additionally, we pay attention to the security of FastDFS from a deterministic point of view. Utilizing the Process Analysis Toolkit (PAT) as a model checker, we employ the constructed model to validate several internal properties and security properties, including Deadlock Freedom, Divergence Freedom, Reachability, Robustness, Consistency, Eagerly Secure, Lazily Secure and Mixed Secure. Our final verification results demonstrate that the model effectively fulfills the internal properties, indicating that the system can well guarantee the management of files. However, it cannot cater to the security properties, which means the model implies some potential security vulnerabilities from a deterministic point of view.

Business Process Model and Notation (BPMN) has been widely adopted as the international standard for business process modeling in enterprise applications. However, existing BPMN models lack rigorous semantic definitions, leading to significant challenges in correctness verification, including deadlock detection and data conflict analysis. Divergent implementations across execution engines further exacerbate such ambiguities. To address these gaps, this paper proposes BDafny: a formal execution and verification framework for BPMN 2.0. Based on Dafny, the verification-aware language, BDafny provides: (1) Executable formalization of BPMN 2.0 semantics for Hoare-logic based behavioral reasoning. (2) Automated and proven detection of practical modeling errors. (3) Multi-target code generation for portable process deployment. By bridging formal methods with industrial standards, BDafny contributes a mechanically verified foundation for BPMN semantics, supporting correct-by-construction automation of business processes.

Cloud communication, as a core component of the cloud computing architecture, relies on the communication mechanism of TCP/UDP protocols. However, with the popularity of cloud communication, the security threats that it faces are also becoming increasingly severe. Graphene is a new cloud communication security architecture that targets both TCP and UDP communication. It provides security assurance during data transmission and authentication for cloud users and cloud service providers, effectively addressing some of the shortcomings of traditional security protocols. In light of Graphene's advantages, it is gaining increasing attention from industries. Hence, ensuring the reliability of Graphene becomes paramount.In this paper, we first utilize process algebra CSP to model the TCP-based communication processes within the Graphene architecture. Subsequently, we model the UDP-based communication processes as well. Then, we employ the model checker PAT to run the CSP models for both protocols and subsequently verify six properties: Deadlock Freedom, Divergence Freedom, Data Reachability, Cloud User Faking, Cloud Instance Faking, and Central Key Server Faking. According to the verification results, our models for both TCP and UDP satisfy all of the aforementioned properties. Therefore, we can conclude that the communication execution processes for both TCP and UDP in the Graphene architecture fulfill the anticipated security standards, thus indicating the reliability of the system.

Verilog is a hardware description language (HDL) that has become an industry-standard HDL of IEEE. Multithreaded discrete event simulation language (MDESL) is a Verilog-like language. Previously, we have studied the operational semantics and denotational semantics for MDESL. This article investigates the soundness and completeness of the operational semantics for MDESL based on the denotational semantics. We introduce the concepts of transitional condition and phase semantics for each transition to show the relationship between a transition and variables in the denotational model. Then, we give the definition for the soundness and completeness of the operational semantics for MDESL. Based on our definition of the operational semantics of MDESL, we investigate the detailed theoretical proof for the soundness and completeness. Finally, a practical approach complements the theoretical one. We apply the proof assistant Coq to verify the soundness and completeness of the operational semantics for MDESL. Our research demonstrates the consistency between operational and denotational semantics for MDESL through theoretical and practical approaches.

Communicating Sequential Processes (CSP) is a formal language used in modeling and verifying concurrent systems and protocols. However, manually constructing a CSP model is typically time-consuming. Recent advancements in Large Language Models (LLMs) show potential for automatically transforming requirements in natural language into formal specifications. In this paper, we propose the first datasets of CSP: CSP#-PAT-84 and CSP#-Handwrite-45, containing a total of 129 models and 1375 processes in a machine-readable syntax CSP#. The CSP#-PAT-84 dataset comprises CSP models from examples in the Process Analysis Toolkit (PAT) and covers five categories. The CSP#-Handwrite-45 dataset consists of CSP models extracted from research papers focusing on practical protocols, algorithms, and systems. Moreover, we introduce NL2CSP, a multi-stage approach designed to improve the performance of LLMs in generating codes in CSP#. Experiments are conducted on both the process generation and model generation tasks to evaluate the capability of LLMs to generate correct CSP processes and models, as well as to establish a benchmark for future research. The results demonstrate that with the capability of in-context learning, LLMs can understand most of the requirements written in natural language and generate corresponding CSP processes and models.

New Simple Queue (NSQ) is a distributed messaging platform developed in Golang that can handle billions of daily messages. Its distributed architecture ensures high fault tolerance and availability. Given NSQ's widespread application across various fields, it is crucial to focus on the system's robustness and data transmission security. Therefore, a rigorous mathematical logic analysis of NSQ's messaging mechanism is essential for verifying its reliability. This paper formalizes NSQ's core components using Communicating Sequential Processes (CSP), resulting in a comprehensive formal model of the system. Furthermore, this paper utilizes the Process Analysis Toolkit (PAT) for practical implementation of the model, verifying five critical properties of the NSQ system. And the verification results demonstrate that the NSQ system successfully satisfies these essential properties, highlighting its flexibility, robustness and efficient messaging service capabilities. Moreover, this paper focuses on formalizing and verifying the security mechanisms in NSQ's data transmission. By integrating the Transport Layer Security (TLS) protocol into the NSQ system and employing a man-in-the-middle model to simulate deception and interception attacks, it is demonstrated that the TLS protocol enhances the security of NSQ data transmission. This paper also proposes upgrading from one-way to two-way certificate authentication to further enhance TLS data security. Experimental results reveal that despite significant security improvements with the TLS protocol, producer and consumer processes remain vulnerable to spoofing attacks under specific insecure network conditions, leading to potential data leaks. Therefore, the TLS protocol can significantly improve the data security of the NSQ system.

The wireless sensor network (WSN) is a foundational technology for the Internet of Things (IoT), and the application of WSN has experienced significant growth in recent years. The MQTT-SN (Message Queuing Telemetry Transport for Wireless Sensor Networks) protocol is widely used to meet the communication needs of low-power, resource-constrained sensor nodes in WSN. These sensor nodes are often exposed to security risks in wireless communication. Therefore, it is important to verify the security of MQTT-SN to ensure the confidentiality and reliability of the network and data. In this paper, we first propose an MQTT-SN application model that combines the MQTT-SN protocol with an efficient and lightweight cryptographic authentication algorithm called ChaCha20-Poly1305. Then, we formalize the proposed model using the process algebra CSP (Communicating Sequential Process). Afterward, we verify whether the model satisfies the five basic properties with the help of the model checker PAT (Process Analysis Toolkit). We further utilize C# to implement the complex functions and data structures in our model. Finally, we introduce four kinds of attacks and incorporate these attacks into the original model. And we verify the corresponding security properties again with PAT to assess the performance of our model under security threats. According to the verification results, our proposed model of the MQTT-SN protocol combined with the ChaCha20-Poly1305 algorithm satisfies all the basic and security properties. It can be concluded that our model demonstrates a high level of security.