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.

AMQP, serving as the application layer standard protocol for advanced message queuing systems, has garnered widespread adoption in middleware systems, including Rab-bitMQ, ActiveMQ, and Qpid. However, the key properties and security of AMQP's messaging mechanism remain unverified. Hence, in this paper, we employ process algebra CSP to formalize the AMQP and verify properties such as deadlock freedom, data reachability, concurrency, sequence consistency, and scala-bility. The verification results indicate that AMQP satisfies these properties, demonstrating the reliability in message transmission. Moreover, to further analyze the security of AMQP messaging mechanism, the intruder model and SSL protocol model are introduced in this work. Meanwhile, the comparison of the verification results with and without SSL is also presented, showing an improvement of the AMQP messaging mechanism security.

Contemporary multiprocessor systems often use weak memory models (WMMs), including Partial Store Order (PSO) in some SPARC implementations. PSO relaxes the store-store constraint by allowing individual cores to use a write buffer for different memory locations. This paper employs the Unifying Theories of Programming (UTP) framework to investigate PSO's trace semantics, acting in the denotational semantics style. In this context, a trace is represented as a sequence of snapshots that track changes in registers, write buffers, and shared memory. Our approach generates the complete set of valid execution outcomes, including potential reorderings, while adhering to proper principles. This paper also introduces a set of algebraic laws tailored for PSO utilizing the concept of ‘head normal form{\prime}. With the introduction of guarded choice, every program can be represented by head normal form. This representation models program execution in the presence of reorderings within the PSO model. Additionally, we also explores the relationship between trace semantics and algebraic semantics, establishing a connection by deriving trace semantics from algebraic semantics.

OpenStack Swift is an object storage system that is part of the open-source cloud platform OpenStack. It adopts a fully symmetric architecture design and is extensively employed in production environments to offer users highly available storage services. In this paper, we model OpenStack Swift's basic architecture, as well as its replication service using communication sequential processes (CSP). Additionally, we extend the audit service in Swift and provide a formal model of it. Various properties of our model are subsequently verified using the model checker PAT. The properties include Deadlock Freedom, Data Reachability, Consistency, Availability, Partition Tolerance (CAP), Basically Available, Soft State, Eventually Consistent (BASE), and Data Integrity. The verification results show that the design of OpenStack Swift satisfies both the CAP and the BASE theories and it achieves Data Integrity. In light of our results, it can be safely concluded that OpenStack Swift provides users with highly available and fault-tolerant services.

Percolator is a distributed transaction model pro-posed by Google to deal with large-scale incremental data of search engines. Based on timestamps, it achieves the snapshot isolation level of multi-version concurrency control. Percolator also inspired distributed transaction models for many databases such as TiDB. In this paper, we model the architecture of Percola-tor using process algebra CSP and implement it with the help of the Process Analysis Toolkit (PAT). Subsequently, we verify and analyze several properties, including deadlock-free, divergence-free, consistency, and snapshot isolation. The verification results show that Percolator satisfies the above properties, but is not serializable, which may lead to data anomalies in some cases.