Blockchain and Satisfiability Modulo Theories for Tender Systems
https://doi.org/10.15514/ISPRAS-2023-35(1)-8
Abstract
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.
Supporting agencies: This research was supported by the Mexican Council CONACYT (1006953) in collaboration with Instituto de Investigaciones en Matemáticas Aplicadas y en Sistemas: Posgrado de Ciencia e Ingeniería de la Computación of the Universidad Nacional Autónoma de México. The work was also supported by UNAM-PAPIIT(IA104122) and UNAM-PAPIIT(TA101021).
About the Authors
René DÁVILA
Universidad Nacional Autónoma de México
Mexico
Mexico
Master degree in Computer Science and Engineering, PhD Student at Research Institute in Applied Mathematics and Systems
Rocío ALDECO-PÉREZ
Universidad Nacional Autónoma de México
Mexico
Mexico
Doctor on Computer Science, Research Associate
Everardo BARCENAS
Universidad Nacional Autónoma de México
Mexico
Mexico
Ph.D., Assistant Professor
References
1. Public tendering rules in the EU. Available at: https://europa.eu/youreurope/business/selling-in-eu/public-contracts/public-tendering-rules/index_en.htm.
2. Huynh T.T., Nguyen T.D., Tan H. A survey on security and privacy issues of blockchain technology. In Proc. of the International Conference on System Science and Engineering (ICSSE), 2019, pp. 362-367,.
3. Road data exchange layer. Available at: https://x-road.global/.
4. Barrett C., Sebastiani R. et al. Satisfiability Modulo Theories. In Handbook of Satisfiability. IOS Press, 2009, pp. 825-885.
5. Limón Y., Bárcenas E., et al. Mu-calculus satisfiability with arithmetic constraints. Programming and Computer Soft-ware, vol. 46, no. 8, 2020, pp. 503-510 / Лимон Й., Барсенас Э. и др.. Выполнимость мю-исчисления с арифметическими ограничениями. Труды ИСП РАН, том 33, вып. 2, 2021 г., стр. 191-200. DOI: 10.15514/ISPRAS–2021–33(2)–12.
6. Medina-Martínez D., Bárcenas E. et al. Database management system verification with separation logics. Programming and Computer Software, vol. 47, no. 8, 2021, pp. 654–672.
7. Nakamoto S. Bitcoin - A Peer-to-Peer Electronic Cash System. Appendix A. The bitcoin whitepaper by Satoshi Nakamoto. In Antonopoulos A. Mastering Bitcoin: Programming the Open Blockchain, 2nd ed. O'Reilly Media, 2017, pp. 323-334
8. Yaga D., Mell P. et al. Blockchain technology overview. arXiv:1906.11078, 2019, 68 p,
9. Ismail L., Materwala H. A review of blockchain archi-tecture and consensus protocols: Use cases, challenges, and solutions, Symmetry, vol. 11, issue 10, 2019, article no. 1198, 44 p.
10. Hyperledger fabric. Available at: https://hyperledger-fabric.readthedocs.io/en/latest/index.html.
11. Grosan C., Abraham A. Rule-Based Expert Systems. Intelligent Systems Reference Library, vol. 17, 2011, pp. 149–185.
12. Bockmayr A., Weispfenning V., Maher M. Solving numerical constraints, In Handbook of Automated Reasoning. Robinson A., Voronkov A. eds. MIT Press, 2001, pp. 751–842.
13. Dávila R., Aldeco-Pérez R., Bárcenas E. Tender system verification with satisfiability modulo theories.Iin Proc. of the 9th International Conference in Software Engineering Research and Innovation (CONISOFT), 2021, pp. 69–78.
14. Dávila R., Aldeco-Pérez R., Bárcenas E. Formal Verification of Blockchain Based Tender Systems. Programming and Computer Software, vol. 48, issue 8, 2022, pp. 566-582.
Review
For citations:
DÁVILA R., ALDECO-PÉREZ R., BARCENAS E. Blockchain and Satisfiability Modulo Theories for Tender Systems. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2023;35(1):113-122. https://doi.org/10.15514/ISPRAS-2023-35(1)-8
Email this article 