{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T15:58:15Z","timestamp":1759939095600,"version":"3.41.2"},"reference-count":45,"publisher":"Frontiers Media SA","license":[{"start":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T00:00:00Z","timestamp":1694649600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["frontiersin.org"],"crossmark-restriction":true},"short-container-title":["Front. Blockchain"],"abstract":"<jats:p>In recent times, the research on blockchain interoperability has gained momentum, enabling the entities from different heterogeneous blockchain networks to communicate with each other seamlessly. Amid the proliferation of blockchain ventures, for ensuring the correctness of inter-blockchain communication protocols, manual checking and testing of all the potential pitfalls and possible inter-blockchain interactions are rarely possible. To ameliorate this, in this paper, we propose a systematic approach to model and formally verify the real-time properties of the pub-sub interoperability protocol, with a special focus on message communication through API calls among publishers, subscribers, and brokers. In particular, we use stochastic timed automata for its modeling, and we prove its correctness with respect to a number of relevant properties using model checking\u2014more specifically, the UPPAAL-SMC model checker. To the best of our knowledge, this is the first proposal of its kind to formally verify the blockchain pub-sub interoperability protocol using model checking.<\/jats:p>","DOI":"10.3389\/fbloc.2023.1248962","type":"journal-article","created":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T13:30:26Z","timestamp":1694698226000},"update-policy":"https:\/\/doi.org\/10.3389\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Formal verification of the pub-sub blockchain interoperability protocol using stochastic timed automata"],"prefix":"10.3389","volume":"6","author":[{"given":"Md Tauseef","family":"Alam","sequence":"first","affiliation":[]},{"given":"Raju","family":"Halder","sequence":"additional","affiliation":[]},{"given":"Abyayananda","family":"Maiti","sequence":"additional","affiliation":[]}],"member":"1965","published-online":{"date-parts":[[2023,9,14]]},"reference":[{"key":"B1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/NTMS.2018.8328737","article-title":"Formal verification of smart contracts based on users and blockchain behaviors models","volume-title":"2018 9th IFIP international conference on new Technologies, mobility and security (NTMS)","author":"Abdellatif","year":"2018"},{"key":"B2","unstructured":"Acorn2014"},{"key":"B3","doi-asserted-by":"publisher","first-page":"8163","DOI":"10.1109\/access.2022.3141982","article-title":"Formal modeling and verification of a blockchain-based crowdsourcing consensus protocol","volume":"10","author":"Afzaal","year":"2022","journal-title":"IEEE Access"},{"key":"B4","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/j.jnca.2019.06.018","article-title":"Blockchain for smart communities: applications, challenges and opportunities","volume":"144","author":"Aggarwal","year":"2019","journal-title":"J. Netw. Comput. Appl."},{"key":"B5","doi-asserted-by":"crossref","first-page":"5278","DOI":"10.24251\/HICSS.2020.650","article-title":"Formal verification of functional requirements for smart contract compositions in supply chain management systems","volume-title":"Proc. Of the 53rd Hawaii international conference on system sciences","author":"Alqahtani","year":"2020"},{"key":"B6","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/978-3-319-10512-3_2","article-title":"Modeling bitcoin contracts by timed automata","volume-title":"International conference on formal modeling and analysis of timed systems","author":"Andrychowicz","year":"2014"},{"key":"B7","first-page":"541","article-title":"A formal model of bitcoin transactions","volume-title":"Financial cryptography and data security: 22nd international conference, FC 2018, nieuwpoort, cura\u00e7ao, february 26\u2013march 2, 2018, revised selected papers 22","author":"Atzei","year":"2018"},{"key":"B8","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1145\/3185089.3185138","article-title":"Formal modeling and verification of smart contracts","volume-title":"Proceedings of the 2018 7th international conference on software and computer applications","author":"Bai","year":"2018"},{"key":"B9","doi-asserted-by":"publisher","first-page":"8","DOI":"10.3389\/fbloc.2019.00008","article-title":"Formal models of bitcoin contracts: A survey","volume":"2","author":"Bartoletti","year":"2019","journal-title":"Front. Blockchain"},{"key":"B10","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","article-title":"A tutorial on uppaal","volume":"3185","author":"Behrmann","year":"2004","journal-title":"Formal methods Des. real-time Syst."},{"key":"B11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3471140","article-title":"A survey on blockchain interoperability: past, present, and future trends","volume":"54","author":"Belchior","year":"2021","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"B12","first-page":"87","volume-title":"Timed automata: Semantics, algorithms and tools","author":"Bengtsson","year":"2004"},{"key":"B13","doi-asserted-by":"crossref","first-page":"424","DOI":"10.1145\/3519270.3538468","article-title":"Brief announcement: holistic verification of blockchain consensus","volume-title":"Proceedings of the 2022 ACM symposium on principles of distributed computing","author":"Bertrand","year":"2022"},{"volume-title":"Closure: The definitive guide: Google tools to add power to your javascript","year":"2010","author":"Bolin","key":"B14"},{"key":"B15","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/978-1-4757-4070-7_6","article-title":"Stochastic timed automata","volume-title":"Introduction to discrete event systems","author":"Cassandras","year":"1999"},{"key":"B16","article-title":"Double-spending analysis of bitcoin","volume-title":"Pacific asia conference on information systems proceedings (association for information systems)","author":"Chaudhary","year":"2020"},{"key":"B17","doi-asserted-by":"crossref","DOI":"10.4204\/EPTCS.196.5","volume-title":"Modeling and verification of the bitcoin protocol","author":"Chaudhary","year":"2015"},{"key":"B18","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","article-title":"Model checking and abstraction","volume":"16","author":"Clarke","year":"1994","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"B19","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","article-title":"Uppaal smc tutorial","volume":"17","author":"David","year":"2015","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"B20","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1109\/Blockchain50366.2020.00051","article-title":"Model checking bitcoin and other proof-of-work consensus protocols","volume-title":"2020 IEEE international conference on blockchain (blockchain)","author":"DiGiacomo-Castillo","year":"2020"},{"key":"B21","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1145\/3417310.3431398","article-title":"Performance analysis of hyperledger fabric 2.0 blockchain platform","volume-title":"Proceedings of the workshop on cloud continuum services for smart IoT systems","author":"Dreyer","year":"2020"},{"key":"B22","first-page":"350","article-title":"A distributed blockchain model of selfish mining","volume-title":"International symposium on formal methods","author":"Eijkel","year":"2019"},{"key":"B23","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/978-3-642-18638-7_6","article-title":"Graphviz and dynagraph\u2014Static and dynamic graph drawing tools","volume-title":"Graph drawing software","author":"Ellson","year":"2004"},{"key":"B24","unstructured":"Esprima2015"},{"key":"B25","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/978-3-319-77935-5_11","article-title":"Twenty percent and a few days\u2013optimising a bitcoin majority attack","volume-title":"NASA formal methods symposium","author":"Fehnker","year":"2018"},{"key":"B26","unstructured":"Hyperledger foundation\n            FoundationT. L.\n          2015"},{"volume-title":"A pub-sub architecture to promote blockchain interoperability","year":"2021","author":"Ghaemi","key":"B27"},{"volume-title":"Compositional model checking of consensus protocols specified in tla+ via interaction-preserving abstraction","year":"2022","author":"Gu","key":"B28"},{"key":"B29","doi-asserted-by":"publisher","first-page":"102857","DOI":"10.1016\/j.jnca.2020.102857","article-title":"Survey on blockchain based smart contracts: applications, opportunities and challenges","volume":"177","author":"Hewa","year":"2021","journal-title":"J. Netw. Comput. Appl."},{"key":"B30","first-page":"1","article-title":"A journey of web and blockchain towards the industry 4.0: an overview","volume-title":"2019 international conference on innovative computing (ICIC)","author":"Khan","year":"2019"},{"key":"B31","doi-asserted-by":"publisher","first-page":"19","DOI":"10.3390\/systems10010019","article-title":"Verifying the smart contracts of the port supply chain system based on probabilistic model checking","volume":"10","author":"Liu","year":"2022","journal-title":"Systems"},{"key":"B32","doi-asserted-by":"crossref","first-page":"446","DOI":"10.1007\/978-3-030-32101-7_27","article-title":"Verisolid: correct-by-design smart contracts for ethereum","volume-title":"International conference on financial cryptography and data security","author":"Mavridou","year":"2019"},{"key":"B33","article-title":"Re: bitcoin p2p e-cash paper","author":"Nakamoto","year":"2008","journal-title":"Cryptogr. Mail. List"},{"key":"B34","doi-asserted-by":"publisher","first-page":"8151","DOI":"10.1109\/access.2022.3143145","article-title":"Formal verification of blockchain smart contracts via atl model checking","volume":"10","author":"Nam","year":"2022","journal-title":"IEEE Access"},{"key":"B35","first-page":"980","article-title":"Model-checking of smart contracts","volume-title":"2018 IEEE international conference on iThings & GreenCom & CPSCom & SmartData","author":"Nehai","year":"2018"},{"key":"B36","doi-asserted-by":"publisher","first-page":"101129","DOI":"10.1016\/j.pmcj.2020.101129","article-title":"Model checking smart contracts for ethereum","volume":"63","author":"Osterland","year":"2020","journal-title":"Pervasive Mob. Comput."},{"key":"B37","doi-asserted-by":"crossref","first-page":"48","DOI":"10.23919\/ICACT53585.2022.9728854","article-title":"Formal modeling of smart contract-based trading system","volume-title":"2022 24th international conference on advanced communication technology (ICACT)","author":"Park","year":"2022"},{"key":"B38","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1109\/SFCS.1977.32","article-title":"The temporal logic of programs","volume-title":"18th annual symposium on foundations of computer science (sfcs 1977)","author":"Pnueli","year":"1977"},{"key":"B39","first-page":"216","article-title":"Constructing the call graph of a program","volume-title":"IEEE transactions on software engineering SE-5","author":"Ryder","year":"1979"},{"key":"B40","unstructured":"Surya, the sun god: A solidity inspector2018"},{"key":"B41","unstructured":"The callgraphjs tool2014"},{"key":"B42","unstructured":"The code2flow tool2021"},{"key":"B43","unstructured":"The javascript explorer callgraph tool2018"},{"key":"B44","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3464421","article-title":"A survey of smart contract formal specification and verification","volume":"54","author":"Tolmach","year":"2021","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"B45","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-981-15-9213-3_1","article-title":"Modeling and verification of the nervos ckb block synchronization protocol in uppaal","volume-title":"International conference on blockchain and trustworthy systems","author":"Zhang","year":"2020"}],"container-title":["Frontiers in Blockchain"],"original-title":[],"link":[{"URL":"https:\/\/www.frontiersin.org\/articles\/10.3389\/fbloc.2023.1248962\/full","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T13:30:43Z","timestamp":1694698243000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.frontiersin.org\/articles\/10.3389\/fbloc.2023.1248962\/full"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,14]]},"references-count":45,"alternative-id":["10.3389\/fbloc.2023.1248962"],"URL":"https:\/\/doi.org\/10.3389\/fbloc.2023.1248962","relation":{},"ISSN":["2624-7852"],"issn-type":[{"type":"electronic","value":"2624-7852"}],"subject":[],"published":{"date-parts":[[2023,9,14]]},"article-number":"1248962"}}