Formalising a Gateway-based Blockchain Interoperability Solution with Event-B (Replication package)

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.

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 of the gateway-based interoperability solution proposed by Pandolfi et al.. 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.