Блокчейн и задача выполнимости формул в теориях для тендерных систем

В тендерном процессе участвуют конкурирующие предложения от разных кандидатов – поставщиков или их контрагентов. Победитель тендера должен поставить или оказать услугу на лучших условиях, чем конкуренты. Тендеры разрабатываются с использованием централизованных непроверенных систем, что снижает прозрачность, справедливость и доверие к процессу, а также снижает возможность обнаружения злонамеренных попыток манипулирования процессом. Системы, которые обеспечивают формальную проверку, децентрализацию, аутентификацию, доверие и прозрачность, могут снизить эти риски. Задача выполнимости формул в теориях обеспечивает формальный анализ для доказательства правильности свойств тендерных предложений, проверенные свойства обеспечивают надежность системы. Кроме того, одной из технологий, обеспечивающих децентрализацию, является блокчейн, цепочка распределенных и децентрализованных записей, связанных таким образом, что обеспечивается целостность. В нашей статье представлена формальная проверенная и децентрализованная система управления тендерными предложениями, основанная на задаче выполнимости формул в теориях и технологии блокчейн и направленная на то, чтобы сделать электронные тендеры на закупки более надежными, прозрачными и справедливыми.

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.