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.

The Advanced Message Queuing Protocol (AMQP), an application-layer protocol based on the publish/subscribe model, is widely used in the field of distributed communication.To verify the correctness of its messaging mechanism and crashhandling mechanism, this paper employs the Multiparty Session Types (MPST) theory and the mpstk toolkit to formally model and verify the AMQP protocol.This paper introduces crash scenarios into the AMQP protocol and verifies the safety, deadlockfreedom, and liveness of both the protocol's messaging mechanism and crash-handling mechanism.The verification results demonstrate that the messaging mechanism and crash-handling mechanism of the AMQP protocol satisfy the aforementioned properties, proving its reliability.

With the booming development of Internet of Things (IoT), the LoRaWAN protocol, a crucial technology in Low Power Wide Area Network (LPWAN), has attracted academic attention. Numerous studies on the security of LoRaWAN have been proposed, and some of these studies have been rigorously verified. However, there is a lack of a unified verification framework for the LoRaWAN protocol. In this paper, we present a unified, comprehensive, and systematic security verification framework for the LoRaWAN protocol. The framework facilitates the construction of CSP model for the LoRaWAN protocol and enables the implementation of these CSP models in PAT with C#. Additionally, it supports the formal verification of the models. By integrating C# into PAT, our framework gains extensibility, flexibility, and broad applicability. Simultaneously, we introduce intruders in our CSP model to simulate five different types of attacks (Replay attacks, DoS attacks, ACK Spoofing attacks, Bit Flipping attacks, and MITM attacks) to evaluate LoRaWAN’s performance in vulnerable environments. To demonstrate the applicability of our framework, we extend it to higher versions of LoRaWAN and apply it in the manufacturing industry. We not only verify the fundamental properties but also validate the security properties by simulating attacks in PAT. Our work would help to diversely analyze the security aspects related to the LoRaWAN protocol, and provide the foundation for the analysis of enhancing its security and robustness.

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.

The C and C++ languages introduced the relaxed-memory concurrency into the language specification for efficiency purposes in 2011. Trace semantics can provide the mathematical foundation for the proposed C++11 memory model, and there is a lack of investigation of trace semantics for C++11. The Promising Semantics (PS) of Kang et al. provides the standard SC-style operational semantics for the C++11 concurrency model, where “SC” refers to “Sequential Consistency”. Inspired by PS, in this article we first investigate the trace semantics for the relaxed read and write accesses under C++11, acting in the denotational semantics style. In our semantic model, a trace is in the form of a sequence of snapshots, and the snapshots record the modification in the relevant global or local variables, and the thread view. Moreover, the trace semantics for the release/acquire accesses under C++11 is also explored, based on the separated thread views and newly added message views. When considering this trace model, different accesses bring in their unique snapshots, and make distinguished effects on the production of the sequences. For any given program, the proposed trace semantics in this article produces all the valid traces directly. Furthermore, our trace semantics, together with that for TSO and MCA ARMv8, has the possibility to be the foundation of the meta model of the trace semantics for weak memory models.

With the flourish of the Internet of Things (IoT), the group communication Constrained Application Protocol (CoAP) emerged at the historic moment, enabling homogeneous devices with constrained computing ability to communicate with ease. CoAP is widely used in transportation, health care and many other aspects. Hence, it is prominent to propose a flexible and efficient architecture for usage in such scenarios and study the data security and consistency of the architecture from the perspective of formal methods. In this paper, we extend the group communication CoAP model to the enhanced group communication CoAP by the introduction of smart gateways and binding to new security suites. We make further improvements to increase the scalability and flexibility of the architecture, making it more applicable in a healthcare scenario or smart home scenario. And we adopt process algebra Communicating Sequential Processes (CSP) with real-time extension to model the enhanced group communication CoAP. We use model checker PAT to verify eight properties of our model on an abstract level, including four basic properties and four security properties. We also conduct a simulation on the local machine for validation of the above properties on a more detailed level. Despite some simplifications of physical properties, both results of the verification and simulation show that the proposed architecture can satisfy those requirements and demonstrate a good possibility of being securely put into service.

Nowadays, the utilization of online auction platforms is becoming increasingly prevalent.Online auction provides a common and practical way for global buyers to compete fairly.Nevertheless, the anonymous environment may bring collusion among entities with effects on results.Compared with traditional mechanisms which rely on third-party platforms, the data auction based on smart contract can create a decentralized environment to avoid the occurrence of collusion.Meanwhile, there exists few research on the verification of its reliability and safety which is worth investigating from the perspective of formal methods.In this paper, we apply Process Algebra CSP in modeling the data auction communicating system among five key entities.In addition, we use Process Analysis Toolkit (PAT) to realize the mechanism and verify five crucial properties, including deadlock freedom, data reachability, data correctness, anti-collusion capability and data security.The verification results indicate that the architecture of data auction based on smart contract can satisfy all the above requirements.Especially, the design of asymmetric encryption for the fundamental information ensures the non-occurrence of collusion in the auction.Additionally, the digital signature generated by private key attached to the message guarantees the safety of the interaction.