{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,13]],"date-time":"2026-04-13T20:58:37Z","timestamp":1776113917540,"version":"3.50.1"},"reference-count":77,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100020901","name":"Deanship of Scientific Research, Islamic University of Madinah, Madinah, Saudi Arabia","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100020901","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2026]]},"DOI":"10.1109\/access.2026.3680617","type":"journal-article","created":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T19:54:26Z","timestamp":1775246066000},"page":"53667-53697","source":"Crossref","is-referenced-by-count":0,"title":["Formal Modeling and Verification of Block Production BABE Protocol in Polkadot"],"prefix":"10.1109","volume":"14","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-8780-5480","authenticated-orcid":false,"given":"Muhammad","family":"Rashid","sequence":"first","affiliation":[{"name":"Department of Computer Science, IBADAT International University Islamabad, Pakpattan Campus, Pakistan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1679-6851","authenticated-orcid":false,"given":"Nazir Ahmad","family":"Zafar","sequence":"additional","affiliation":[{"name":"Department of Computer Science, COMSATS University Islamabad, Sahiwal Campus, Pakistan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Waheed","family":"Shahzad","sequence":"additional","affiliation":[{"name":"Department of Computer Science, IBADAT International University Islamabad, Pakpattan Campus, Pakistan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1624-7580","authenticated-orcid":false,"given":"Lal","family":"Khan","sequence":"additional","affiliation":[{"name":"Department of AI and SW, Gachon University, Seongnam, Republic of Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohammad Zubair","family":"Khan","sequence":"additional","affiliation":[{"name":"Faculty of Computer and Information Systems, Islamic University of Madinah, Madinah, Saudi Arabia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ibrahim","family":"Aljubayri","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Information, Imam Mohammad Ibn Saud Islamic University (IMSIU), Riyadh, Saudi Arabia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1504\/IJWGS.2018.095647"},{"key":"ref2","author":"Nakamoto","year":"2008","journal-title":"Bitcoin Whitepaper"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/MCSE.2017.3421554"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1108\/SCM-03-2018-0143"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/ICSEngT.2019.8906403"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1155\/2022\/3727389"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2022.3180168"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosust.2017.04.011"},{"issue":"22","key":"ref9","first-page":"5","article-title":"Ethereum white paper","volume":"1","author":"Buterin","year":"2013","journal-title":"GitHub Repository"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22846-4_10"},{"key":"ref11","volume-title":"Litecoin: An Introduction to Litecoin Cryptocurrency and Litecoin Mining","author":"Reed","year":"2017"},{"issue":"2327","key":"ref12","first-page":"4662","article-title":"Polkadot: Vision for a heterogeneous multi-chain framework","volume":"21","author":"Wood","year":"2016","journal-title":"White paper"},{"key":"ref13","article-title":"Overview of polkadot and its design considerations","author":"Burdges","year":"2020","journal-title":"arXiv:2005.13456"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.cie.2023.109347"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/Blockchain55522.2022.00019"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v38i9.28807"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363278"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4842-8179-6_8"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1186\/s42400-025-00417-x"},{"key":"ref20","article-title":"Can Byzantine fault tolerant consensus agreement be utilitarian, scalable and resilient? An algorithm proposition from a consortium blockchain perspective: Cuba","author":"Samuel","year":"2024"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2022.3228535"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/BCCA58897.2023.10338906"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0058022"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1088\/1757-899X\/734\/1\/012152"},{"key":"ref25","first-page":"118","article-title":"The truth about blockchain","author":"Iansiti","year":"2017","journal-title":"Harvard Bus. Rev."},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/ICBC54727.2022.9805554"},{"key":"ref27","first-page":"9:1","article-title":"On the formal verification of the stellar consensus protocol","volume-title":"Proc. 2nd Workshop Formal Methods Blockchains (FMBC)","author":"Losa"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/ITME.2018.00196"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_8"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"ref31","first-page":"8","article-title":"Formal specification and model checking of the tendermint blockchain synchronization protocol (short paper)","volume-title":"Proc. 2nd Workshop Formal Methods Blockchains (FMBC)","author":"Braithwaite"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS2018.2018.00031"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54994-7_27"},{"key":"ref34","article-title":"Formal verification of blockchain Byzantine fault tolerance","author":"Tholoniat","year":"2019","journal-title":"arXiv:1909.07453"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.342.6"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/IWBOSE.2019.8666514"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2023.103290"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2022.3141982"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1016\/j.comcom.2022.06.014"},{"key":"ref40","article-title":"Formally verified blockchain consensus","author":"P\u00eerlea","year":"2019"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/3519270.3538468"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.18255\/1818-1015-2020-4-454-471"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-93706-4_9"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.3390\/math9222954"},{"key":"ref45","first-page":"1","article-title":"Formally verifying the safety of pipelined moonshot consensus protocol","volume-title":"Proc. ACM Program. Lang.","author":"Praveen"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1109\/ICBC48266.2020.9169472"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/3520084.3520100"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/3729306"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.23919\/FRUCT65909.2025.11007982"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/s10586-024-04923-4"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2022.111445"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.5220\/0013291000003928"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2024.3363833"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2952635"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-15-5682-1_55"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1109\/TSC.2025.3547222"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2024.3404103"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1109\/TrustCom60117.2023.00298"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1109\/GLOBECOM42002.2020.9322354"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2024.3349654"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-67321-4_6"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1109\/ICOSST60641.2023.10414247"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1109\/ICET59753.2023.10374485"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1109\/FIT60620.2023.00055"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1109\/KHI-HTC60760.2024.10481884"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.3390\/app15052487"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-87675-3_1"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.3311\/PPtr.23344"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.26408\/125.01"},{"key":"ref70","article-title":"A case study on model checking and runtime verification for awkernel","author":"Hasegawa","year":"2025","journal-title":"arXiv:2503.09282"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1016\/j.ssci.2018.05.009"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2025.3540428"},{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1016\/j.inffus.2023.102048"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.37745\/ejcsit.2013\/vol13n203041"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2007.1021"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.28"},{"key":"ref77","doi-asserted-by":"publisher","DOI":"10.1109\/FormaliSE.2017.9"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/6287639\/11323511\/11474461.pdf?arnumber=11474461","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,13]],"date-time":"2026-04-13T19:37:51Z","timestamp":1776109071000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11474461\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"references-count":77,"URL":"https:\/\/doi.org\/10.1109\/access.2026.3680617","relation":{},"ISSN":["2169-3536"],"issn-type":[{"value":"2169-3536","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]}}}