# Formalising a Gateway-based Blockchain Interoperability Solution with Event-B (Replication package)
# 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](https://icbc2025.ieee-icbc.org/workshop/crosschain).
## Introduction
This repository holds the artefacts that raised the results of our first paper _Formalising a Gateway-based Blockchain Interoperability Solution with Event-B_ to be presented at the [ICBC Cross-chain workshop](https://icbc2024.ieee-icbc.org/workshop/crosschain).
In this paper, we explore to what extent, Event-B could help us to formalise the Temporal Transfer Pattern proposed in a [previous work](https://ieeexplore.ieee.org/document/10628270/). 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. On the other hand, the experiment also revealed challenges. Cross-chain safety properties required additional effort to build an understandable specification. Expressing these properties required the use of Event-B theorems due to its complexity, as they involve multiple events. Event-B invariants, while sufficient in other contexts, were insufficient to keep an understandable specification.
In this paper, we explore the formalisation of a gateway-based interoperability solution with Event-B. The results showed that the method was suitable and that a straightforward specification could be developed considering Ethereum and Hyperledger Fabric as the involved blockchains. The Event-B specification was assessed with three strategies that enabled its verification and validation. In particular, formal verification (e.g. safety properties), functional validation, and functional utility. These promising results constitute a step forward in the development of formal specifications for blockchain interoperability solutions.
The artefacts generated in this research were:
-[An Event-B specification](Temporal_Transfer_Pattern_Specification.pdf) 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.
-[An Event-B specification](Gateway_Event_B_specification.pdf) of the gateway-based interoperability solution proposed by [Pandolfi et al.](https://ieeexplore.ieee.org/document/10346168). This specification is composed of three machines: an abstract machine and two refinements. One refinement describes the behaviour of the gateway and smart contracts involved when the source blockchain is Ethereum and the target blockchain is Hyperledger Fabric. The second refinement describes the behaviour of the gateway and smart contracts when the source is Hyperledger Fabric and the target Ethereum.
- Animations of the three specifications (i.e. abstract and refinements) that enabled us to validate the functional behaviour of the specification and provided the means to understand the gateways' behaviour without Event-B knowledge.
-An Event-B specficiation of a use case scenario that shows the utility of the specification.
