Formal Development of Blockchain Enabled E Healthcare System Using Event-B

Formal Development of Blockchain Enabled E Healthcare System Using Event-B

  IJETT-book-cover           
  
© 2025 by IJETT Journal
Volume-73 Issue-2
Year of Publication : 2025
Author : Raghuraj Singh Suryavanshi, Vishal Nagar, Abhishek Rawat, Divakar Yadav
DOI : 10.14445/22315381/IJETT-V73I2P110

How to Cite?
Raghuraj Singh Suryavanshi, Vishal Nagar, Abhishek Rawat, Divakar Yadav, "Formal Development of Blockchain Enabled E Healthcare System Using Event-B," International Journal of Engineering Trends and Technology, vol. 73, no. 2, pp. 119-134, 2025. Crossref, https://doi.org/10.14445/22315381/IJETT-V73I2P110

Abstract
Developing complicated systems makes correct software development a difficult process. Software may contain imperfections as a result of incorrect specifications. Traditional testing procedures are insufficient to ensure the proper functioning of a complicated system. Formal approaches are essential to capture accurate system requirements and accurate logic about the challenges. Formal methods are a mathematical approach that provides issued specifications, solutions, and verification of correctness. This paper presents the formal verification of the Blockchain Enabled Electronic Health Record System using Event-B, implemented in Remix IDE using Blockchain Technology. Blockchain technology ensures transparency and integrity while securely storing and exchanging patient data. Its decentralized structure can facilitate smooth interoperability between healthcare providers, improve data security, and streamline operations. Event B is a formal technique for system-level modeling. It is a mathematical and formal notation that allows complicated systems to be specified, refined, and verified. This paper aims to use blockchain technology and a formal verification process for developing the Electronic health record system with proof of obligation and provide secure data storage by defining easy access rules for the users of the proposed framework. This work is to provide the electronic health record system with the benefits of scalable, secure, transparent, and integral blockchain-based solutions.

Keywords
Blockchain technology, E-Healthcare system, Event-B, Formal methods, Smart contract.

References
[1] Asma Khatoon, “A Blockchain-based Smart Contract System for Healthcare Management,” Electronics, vol. 9, no. 1, pp. 1-23, 2020.
[CrossRef] [Google Scholar] [Publisher Link]
[2] M. Sumathi et al., “Appointment Booking and Drug Inventory System in Healthcare Services using Blockchain Technology,” ADCAIJ: Advances in Distributed Computing and Artificial Intelligence Journal, vol. 12, no. 1, pp. 1-16, 2023.
[CrossRef] [Google Scholar] [Publisher Link]
[3] Hengrui Jia et al., “Proof-of-Learning: Definitions and Practice,” IEEE Symposium on Security and Privacy (SP), San Francisco, CA, USA, pp. 1039-1056, 2021.
[CrossRef] [Google Scholar] [Publisher Link]
[4] John von Neumann, The General and Logical Theory of Automata, Systems Research for Behavioral Science, Routledge, pp. 97-107, 2017.
[Google Scholar] [Publisher Link]
[5] Shahid Khan, Osman Hasan, and Atif Mashkoor, “Formal Verification and Safety Assessment of a Hemodialysis Machine,” International Conference on Current Trends in Theory and Practice of Informatics, Springer International Publishing, pp. 241-254, 2017.
[CrossRef] [Google Scholar] [Publisher Link]
[6] Sulskus Gintautas, “An Investigation into Event-B Methodologies and Timing Constraint Modeling,” Doctoral Dissertation, University of Southampton, pp. 1-217, 2017.
[Google Scholar] [Publisher Link]
[7] Racem Bougacha et al., “Extending SysML with Refinement and Decomposition Mechanisms to Generate Event-b Specifications,” International Symposium on Theoretical Aspects of Software Engineering, Springer International Publishing, pp. 256-273, 2022.
[CrossRef] [Google Scholar] [Publisher Link]
[8] Ariel Ekblaw et al., “A Case Study for Blockchain in Healthcare: “MedRec” Prototype for Electronic Health Records and Medical Research Data,” Proceedings of IEEE Open & Big Data Conference, vol. 13, 2016.
[Google Scholar]
[9] Sabita Khatri et al., “A Systematic Analysis on Blockchain Integration with Healthcare Domain: Scope and Challenges,” IEEE Access, vol. 9, pp. 84666-84687, 2021.
[CrossRef] [Google Scholar] [Publisher Link]
[10] Mohan Kubendiran, Satyapal Singh, and Arun Kumar Sangaiah, “Enhanced Security Framework for E-Health Systems using Blockchain,” Journal of Information Processing Systems, vol. 15, no. 2, pp. 239-250, 2019.
[CrossRef] [Google Scholar] [Publisher Link]
[11] A.G. Chandini, and P.I. Basarkod, “Patient Centric Pre-Transaction Signature Verification Assisted Smart Contract based Blockchain for Electronic Healthcare Records,” Journal of Ambient Intelligence and Humanized Computing, vol. 14, no. 4, pp. 4221-4235, 2023.
[CrossRef] [Google Scholar] [Publisher Link]
[12] Mouhamad Almakhour et al., “Verification of Smart Contracts: A Survey,” Pervasive and Mobile Computing, vol. 67, 2020.
[CrossRef] [Google Scholar] [Publisher Link]
[13] Palina Tolmach et al., “A Survey of Smart Contract Formal Specification and Verification,” ACM Computing Surveys (CSUR), vol. 54, no. 7, pp. 1-38. 2021.
[CrossRef] [Google Scholar] [Publisher Link]
[14] Yuepeng Wang et al., “Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain,” Verified Software. Theories, Tools, and Experiments: 11th International Conference, New York City, NY, USA, pp. 87-106, 2020.
[CrossRef] [Google Scholar] [Publisher Link]
[15] Ikram Garfatta et al., “A Survey on Formal Verification for Solidity Smart Contracts,” Proceedings of the Australasian Computer Science Week Multiconference, pp. 1-10, 2021.
[CrossRef] [Google Scholar] [Publisher Link]
[16] Leonardo Alt, and Christian Reitwiessner, “SMT-based Verification of Solidity Smart Contracts,” Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice: 8th International Symposium, ISoLA, Limassol, Cyprus, pp. 376-388, 2018.
[CrossRef] [Google Scholar] [Publisher Link]
[17] Anu Raj, and Shiva Prakash, “Smart Contract-based Secure Decentralized Smart Healthcare System,” International Journal of Software Innovation (IJSI), vol. 11, no. 1, pp. 1-20, 2023.
[CrossRef] [Google Scholar] [Publisher Link]
[18] Abid Hassan et al., “Secured Insurance Framework using Blockchain and Smart Contract,” Scientific Programming, vol. 2021, pp. 1-11, 2021.
[CrossRef] [Google Scholar] [Publisher Link]
[19] Sanjeev Kumar Dwivedi et al., “Blockchain‐based Electronic Medical Records System with Smart Contract and Consensus Algorithm in Cloud Environment,” Security and Communication Networks, vol. 2022, pp. 1-10, 2022.
[CrossRef] [Google Scholar] [Publisher Link]
[20] Eman H. Alkhammash, “Trustworthy Smart City Systems using Refinement and Event-B Theories,” Multimedia Tools and Applications, vol. 81, no. 1, pp. 615-636, 2022.
[CrossRef] [Google Scholar] [Publisher Link]
[21] Guillaume Dupont et al., “Event-B Hybridation: A Proof and Refinement-based Framework for Modeling Hybrid Systems,” ACM Transactions on Embedded Computing Systems (TECS), vol. 20, no. 4, pp. 1-37, 2021.
[CrossRef] [Google Scholar] [Publisher Link]
[22] Xinpeng Shen et al., “A Novel Method for Causal Structure Discovery from EHR Data and its Application to Type-2 Diabetes Mellitus,” Scientific Reports, vol. 11, no. 1, pp. 1-9, 2021.
[CrossRef] [Google Scholar] [Publisher Link]
[23] Ravi Sharma et al., “Design of Blockchain-based Precision Health-Care using Soft Systems Methodology,” Industrial Management & Data Systems, vol. 120, no. 3, pp. 608-632, 2020.
[CrossRef] [Google Scholar] [Publisher Link]
[24] Na Hong et al., “Integrating Structured and Unstructured EHR Data using an FHIR-based Type System: A Case Study with Medication Data,” AMIA Summits on Translational Science Proceedings, vol. 2018, pp. 74-83, 2018.
[Google Scholar] [Publisher Link]
[25] James Kolapo Oladele et al., “A Blockchain Electronic Health Data System for Secure Medical Records Exchange,” Journal of Computing Theories and Applications, vol. 1, no. 3, pp. 231-242, 2024.
[CrossRef] [Google Scholar] [Publisher Link]