An Approach to Formalise Blockchain Interoperability Patterns (Replication package)

This repository holds the artefacts that raised the results of our paper titled An Approach to Formalise Blockchain Interoperability Patterns to be presented at the ICBC Cross-chain workshop 2025. In this paper, we explore to what extent, Event-B could help us to formalise the Temporal Transfer Pattern proposed in a previous work. In particular, an instantiations based on the gateway approach. The results showed that it was possible to formally specify the Temporal Transfer pattern following the gateway-based approach with Event-B. The resulting specification enabled for a precise modelling of actors, interactions, and eight safety properties, supported by proof obligations that ensures its consistency and correctness. In addition, a simulation-based validation was performed to assess its functional behaviour. Event-B proved to be effective in expressing safety properties involving the composition of multiple events. Finally, refinements enabled model reusability and composition, reducing time and effort. These results are encouraging, as formalising the structural and behavioural aspects of the pattern was direct and effective. The artefacts generated in this research were: An Event-B specification of the Temporal Transfer pattern instantiated using the gateway-based approach. A mockup of the simulations that enabled us to validate the functional behaviour of the specification. This animation mockup provides a quick approach to the comprehension of the pattern without Event-B knowledge. The Event-B project that can be used as foundations for other research projects or run simulations with ProB.本仓库存储了承载将在2025年ICBC跨链研讨会（ICBC Cross-chain workshop 2025）上发表的论文《区块链互操作模式（Blockchain Interoperability Patterns）形式化的一种方法》研究成果的制品。 在本研究中，我们探究了Event-B（Event-B）可在多大程度上助力对过往研究中提出的时间传输模式（Temporal Transfer Pattern）进行形式化建模，尤其是基于网关方法（gateway approach）的实例化场景。研究结果表明，采用Event-B结合网关方法，可以完成时间传输模式的形式化规约构建。最终生成的规约能够精准建模参与者、交互流程以及八项安全属性（safety properties），并通过证明义务（proof obligations）保障规约的一致性与正确性。此外，我们还开展了基于模拟的验证工作，以评估规约的功能行为表现。实践证明，Event-B可有效表达包含多事件组合的安全属性。最终，模型精化（refinements）机制实现了模型的可复用性与组合性，降低了开发时间与人力成本。本研究结果令人鼓舞，因为对该模式的结构与行为层面进行形式化建模的过程直接且高效。 本研究产出的研究制品包括： 采用网关方法实例化的时间传输模式（Temporal Transfer Pattern）Event-B（Event-B）形式化规约。 用于验证该规约功能行为的模拟原型。该动画原型无需掌握Event-B相关知识，即可帮助使用者快速理解该模式的运作逻辑。 可作为其他研究项目基础、或可配合ProB工具开展模拟的Event-B（Event-B）项目文件。