Currently, inter-organizational process collaboration (IOPC) has been widely used in the design and development of distributed systems that support business process execution. Blockchain-based IOPC can establish trusted data sharing among participants, attracting more and more attention. The core of such study is to translate the graphical model (e.g., BPMN) into program code called smart contract that can be executed in the blockchain environment. In this context, a proper smart contract plays a vital role in the correct implementation of block-chain-based IOPC. In fact, the quality of graphical model affects the smart con-tract generation. Problematic models (e.g., deadlock) will result in incorrect contracts (causing unexpected behaviours). To avoid this undesired implementation, this paper explores to generate smart contracts by using the verified formal model as input instead of graphical model. Specifically, we introduce a prototype framework that supports the automatic generation of smart contracts, providing an end-to-end solution from modeling, verification, translation to implementation. One of the cores of this framework is to provide a CSP#-based formalization for the BPMN collaboration model from the perspective of message interaction. This formalization provides precise execution semantics and model verification for graphical models, and a verified formal model for smart contract generation. Another novelty is that it introduces a syntax tree-based translation algorithm to directly map the formal model into a smart contract. The required formalism, verification and translation techniques are transparent to users without imposing additional burdens. Finally, a set of experiments shows the effectiveness of the framework.

翻译：当前，跨组织流程协作（IOPC）已广泛应用于支持业务流程执行的分布式系统设计与开发中。基于区块链的IOPC能够在参与者之间建立可信数据共享，因此受到越来越多的关注。此类研究的核心是将图形化模型（如BPMN）转化为可在区块链环境中执行的程序代码——即智能合约。在此背景下，高质量的智能合约对于正确实现基于区块链的IOPC至关重要。事实上，图形化模型的质量直接影响智能合约的生成。存在问题的模型（例如死锁）会导致错误的合约（进而引发意外行为）。为避免这种不良实现，本文探索以经过验证的形式化模型而非图形化模型作为输入来生成智能合约。具体而言，我们提出一个支持智能合约自动生成的原型框架，提供从建模、验证、转换到实现的端到端解决方案。该框架的核心之一是为BPMN协作模型提供基于CSP#的形式化表达，从消息交互视角出发。这种形式化表达为图形化模型提供了精确的执行语义与模型验证能力，并为智能合约生成提供了经过验证的形式化模型。另一创新之处在于引入基于语法树的转换算法，将形式化模型直接映射为智能合约。所需的形式化、验证与转换技术对用户透明，不增加额外负担。最后，一系列实验证明了该框架的有效性。