Formal Specification and Verification of Replication in Blockchain Oriented Transactional System Using Event-B

Abstract

To deploy a system without checking its correctness is a challenge. Blockchain is a buzzword in the current industry scenario. Blockchain technology is based upon a replicated database in a distributed environment. To verify the existing system, we have formally specified it.  A formal method is a mathematical structure to specify a system. There are multiple formal methods available. Event-B is a formal method, which is used to specify and verify a system of discrete nature. Rodin is an editor, which provides a platform for writing Event-B specifications. After writing B specifications, we have checked the system by the Atelier-B prover.  In this paper, we have done formal specification and verification of the replicated database in a blockchain-oriented transactional system using Event-B.

Keywords: Blockchain, Formal Method, Formal Verification, Event-B, Distributed system, Replicated database