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.