Formal Modeling and Verification of Blockchain Consensus Protocol for IoT Systems

被引:5
|
作者
Baouya, Abdelhakim [1 ]
Chehida, Salim [1 ]
Bensalem, Saddek [1 ]
Bozga, Marius [1 ]
机构
[1] Univ Grenoble Alpes, Verimag Lab, CNRS, Grenoble, France
基金
欧盟地平线“2020”;
关键词
Blockchain; IoT; Statistical Model Checking; Safety; Liveness; TECHNOLOGY; ARCHITECTURE; MANAGEMENT; INTERNET; CHAIN;
D O I
10.3233/FAIA200578
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
Many industrials consider blockchain as a technology breakthrough for cybersecurity, with use cases ranging from cryptocurrency system to smart contracts, and so forth. While IoT systems employ a lightweight communication protocol between physical objects, blockchain may ensure safe information gathering. Unfortunately, the mixture of both technologies has yet to be formally investigated regarding the consensus algorithm. In this paper, statistical model checking is applied to provide quantitative answers on whether the modeled system satisfies safety and liveness properties expressed in LTL temporal logic.
引用
收藏
页码:330 / 342
页数:13
相关论文
共 50 条
  • [1] Formal Modeling and Verification of a Blockchain-Based Crowdsourcing Consensus Protocol
    Afzaal, Hamra
    Imran, Muhammad
    Janjua, Muhammad Umar
    Gochhayat, Sarada Prasad
    [J]. IEEE ACCESS, 2022, 10 : 8163 - 8183
  • [2] Formal verification of persistence and liveness in the trust-based blockchain crowdsourcing consensus protocol
    Afzaal, Hamra
    Imran, Muhammad
    Janjua, Muhammad Umar
    [J]. COMPUTER COMMUNICATIONS, 2022, 192 : 384 - 401
  • [3] Proof of X-repute blockchain consensus protocol for IoT systems
    Wang, Eric Ke
    Sun, RuiPei
    Chen, Chien-Ming
    Liang, Zuodong
    Kumari, Saru
    Khan, Muhammad Khurram
    [J]. COMPUTERS & SECURITY, 2020, 95
  • [4] Formal Modeling and Verification of Blockchain System
    Duan, Zhangbo
    Mao, Hongliang
    Chen, Zhidong
    Bai, Xiaomin
    Hu, Kai
    Talpin, Jean-Pierre
    [J]. PROCEEDINGS OF THE 10TH INTERNATIONAL CONFERENCE ON COMPUTER MODELING AND SIMULATION (ICCMS 2018), 2017, : 231 - 235
  • [5] A Survey of IoT Applications in Blockchain Systems: Architecture, Consensus, and Traffic Modeling
    Lao, Laphou
    Li, Zecheng
    Hou, Songlin
    Xiao, Bin
    Guo, Songtao
    Yang, Yuanyuan
    [J]. ACM COMPUTING SURVEYS, 2020, 53 (01)
  • [6] Verification of customizable blockchain consensus rule using a formal method
    Kawahara, Ryo
    [J]. 2020 IEEE INTERNATIONAL CONFERENCE ON BLOCKCHAIN AND CRYPTOCURRENCY (IEEE ICBC), 2020,
  • [7] Formal Verification of Blockchain Based Tender Systems
    René Dávila
    Rocío Aldeco-Pérez
    Everardo Bárcenas
    [J]. Programming and Computer Software, 2022, 48 : 566 - 582
  • [8] Formal Verification of Blockchain Based Tender Systems
    Davila, Rene
    Aldeco-Perez, Rocio
    Barcenas, Everardo
    [J]. PROGRAMMING AND COMPUTER SOFTWARE, 2022, 48 (08) : 566 - 582
  • [9] Planning for Change in a Formal Verification of the Raft Consensus Protocol
    Woos, Doug
    Wilcox, James R.
    Anton, Steve
    Tatlock, Zachary
    Ernst, Michael D.
    Anderson, Thomas
    [J]. PROCEEDINGS OF THE 5TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP'16), 2016, : 154 - 165
  • [10] Modeling and Verifying the CKB Blockchain Consensus Protocol
    Sun, Meng
    Lu, Yuteng
    Feng, Yichun
    Zhang, Qi
    Liu, Shaoying
    [J]. MATHEMATICS, 2021, 9 (22)