Formal verification of the pub-sub blockchain interoperability protocol using stochastic timed automata

【Author】 Alam, Md Tauseef; Halder, Raju; Maiti, Abyayananda

【Source】FRONTIERS IN BLOCKCHAIN

【影响因子】0.000

【Abstract】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-more 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.

【Keywords】blockchain; chaincode; interoperability; stochastic timed automata; model checking; UPPAAL-SMC

【发表时间】2023 SEP 14

【收录时间】2023-10-06

【文献类型】

【主题类别】

--