Formal Verification of Blockchain Based Tender Systems

被引:1
|
作者
Davila, Rene [1 ]
Aldeco-Perez, Rocio [2 ]
Barcenas, Everardo [2 ]
机构
[1] IIMAS UNAM, Ciudad Univ, Ciudad De Mexico 04510, Cdmx, Mexico
[2] Fac Ingn UNAM, Ciudad Univ, Ciudad De Mexico 04510, Cdmx, Mexico
关键词
Blockchain - Formal verification - Reliability analysis;
D O I
10.1134/S0361768822080096
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
A tender process consists in competing offers from different candidate suppliers or contractors. The tender winner is supposed to supply or provide a service in better conditions than competitors. Tenders are developed using centralized unverified systems, which reduce transparency, fairness and trust on the process, it also reduces the ability to detect malicious attempts to manipulate the process. Systems that provide formal verification, decentralization, authentication, trust and transparency can mitigate these risks. Satisfiability Modulo Theories provides a formal analysis to prove correctness of tender offers properties, verified properties ensures system reliability. In addition, one technology that claims to provide decentralization is Blockchain, a chain of distributed and decentralized records linked in a way such that integrity is ensured. This paper presents a formal verified and decentralized proposal system, based on Satisfiability Modulo Theories and Blockchain technology, to make electronic procurement tenders more reliable, transparent and fair.
引用
收藏
页码:566 / 582
页数:17
相关论文
共 50 条
  • [31] Model based formal verification of distributed production control systems
    Kardos, M
    Rammig, FJ
    INTEGRATION OF SOFTWARE SPECIFICATION TECHNIQUES FOR APPLICATIONS IN ENGINEERING, 2004, 3147 : 451 - 473
  • [32] P systems based computing polynomials: design and formal verification
    Yuan, Weitao
    Zhang, Gexiang
    Perez-Jimenez, Mario J.
    Wang, Tao
    Huang, Zhiwei
    NATURAL COMPUTING, 2016, 15 (04) : 591 - 596
  • [33] Analyzing Learning-Based Networked Systems with Formal Verification
    Dethise, Arnaud
    Canini, Marco
    Narodytska, Nina
    IEEE CONFERENCE ON COMPUTER COMMUNICATIONS (IEEE INFOCOM 2021), 2021,
  • [34] A Blockchain Based Proposal for Protecting Healthcare Systems through Formal Methods
    Brunese, Luca
    Mercaldo, Francesco
    Reginelli, Alfonso
    Santone, Antonella
    KNOWLEDGE-BASED AND INTELLIGENT INFORMATION & ENGINEERING SYSTEMS (KES 2019), 2019, 159 : 1787 - 1794
  • [35] Formal verification of privacy for RFID systems
    Bruso, Mayla
    Chatzikokolakis, Konstantinos
    den Hartog, Jerry
    2010 23RD IEEE COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2010, : 75 - 88
  • [36] Formal verification and analysis of multimedia systems
    Campos, S
    Ribeiro-Neto, B
    Macedo, A
    Bertini, L
    ACM MULTIMEDIA 99, PROCEEDINGS, 1999, : 419 - 430
  • [37] FORMAL SPECIFICATION AND VERIFICATION OF MICROPROCESSOR SYSTEMS
    JOYCE, JJ
    INTEGRATION-THE VLSI JOURNAL, 1989, 7 (03) : 247 - 266
  • [38] FORMAL SPECIFICATION AND VERIFICATION OF MICROPROCESSOR SYSTEMS
    JOYCE, JJ
    MICROPROCESSING AND MICROPROGRAMMING, 1988, 24 (1-5): : 371 - 378
  • [39] Formal Verification of C Systems Code
    Tuch, Harvey
    JOURNAL OF AUTOMATED REASONING, 2009, 42 (2-4) : 125 - 187
  • [40] ON VERIFICATION OF FORMAL MODELS OF COMPLEX SYSTEMS
    Smyrin, A. A. M.
    Lukyanova, E. A.
    TURKISH ONLINE JOURNAL OF DESIGN ART AND COMMUNICATION, 2018, 8 : 348 - 352