Formal Verification of a Medical Insurance System Prototype: The Event-B Modeling Approach.

In worldwide, there is maximizing espousal of blockchain technology by insurers and the healthcare industry. Blockchain has created data silos in the health insurance industry sector. It can solve the most widespread interoperability and non-standardization issues of healthcare information. The formal verification technique can be used to better deal with the smart contracts' correctness, functional accuracy, and safety. We propose a system model of a blockchain-based insurance system. We specify all the requirements using the Event-B modeling language. In Software engineering, we use the formal method or the modeling concept in the early designing and verification stage. So, we can use early verification of the requirements to reduce the inconsistencies between them. For this, we need a specification language like Event-B. This paper uses the Event-B formal verification method to formally model solidity wrote smart contracts to verify and validate their safety, correctness, and functional accuracy for given behaviors. The verification is done with the help of the RODIN tool. [ABSTRACT FROM AUTHOR]