МЕТОДОЛОГІЧНІ АСПЕКТИ ІНТЕГРАЦІЇ ФОРМАЛЬНОЇ ВЕРИФІКАЦІЇ В КОНВЕЄРИ CI/CD: АНАЛІЗ ВИКЛИКІВ І ПЕРСПЕКТИВ

Автор(и)

DOI:

https://doi.org/10.35546/kntu2078-4481.2025.1.2.34

Ключові слова:

формальна верифікація, CI/CD, DevOps, автоматизація, масштабованість, коректність програмного забезпечення, інструменти верифікації, кібербезпека, штучний інтелект, відкриті інструменти

Анотація

Інтеграція формальної верифікації в конвеєри безперервної інтеграції та доставки (CI/CD) є важливим етапом розвитку сучасних методологій розробки програмного забезпечення. У статті аналізуються концептуальні підходи до використання формальних методів для перевірки коректності програмного забезпечення на різних етапах CI/CD-процесів. Розглянуто інструменти та технології, що забезпечують інтеграцію формальної верифікації у цикли DevOps, із акцентом на автоматизації аналізу, масштабованості рішень та забезпеченні відповідності високим стандартам якості.Також у статті детально висвітлено ключові виклики, включаючи складність інтеграції в існуючі інфраструктури, високу обчислювальну вартість формальної верифікації, обмежену доступність спеціалізованих інструментів та необхідність адаптації до специфіки CI/CD-конвеєрів. Особливу увагу приділено питанням забезпечення кібербезпеки, сумісності з розподіленими системами та інтеграції зі штучним інтелектом для підвищення ефективності процесів верифікації.Представлено реальні кейси успішного впровадження формальної верифікації у CI/CD-конвеєри, зокрема у великих технологічних компаніях, таких як Amazon та Microsoft. Проаналізовано можливості поєднання формальних методів із традиційними тестуваннями або підходами, що базуються на машинному навчанні, для підвищення надійності програмного забезпечення.Перспективи розвитку сфокусовано на автоматизації формальної верифікації, удосконаленні інструментарію для складних розподілених систем та розробці адаптивних рішень, що дозволяють масштабувати процеси верифікації в умовах високих обчислювальних навантажень. Окремо розглянуто значення відкритих інструментів і платформ для формальної верифікації, таких як Z3, SPIN і CBMC, що спрощують впровадження даних методів у розробку. Представлені дослідження спрямовані на підвищення надійності, продуктивності та безпеки сучасних програмних систем, а також на досягнення відповідності міжнародним стандартам якості та кібербезпеки.

Посилання

Aichernig, B., Tretter, J., & Wolff, B. (2021). Formal methods in software engineering: Verification and validation approaches. Journal of Software Engineering and Applications, 14(6), 341–358 c.

Clarke, E., Grumberg, O., & Peled, D. (2022). Model checking. MIT Press.

Baier, C., Katoen, J., & Hähnle, R. (2020). Formal verification of software: Challenges and techniques. Formal Methods in System Design, 56(3), 248–272 c.

Bjørner, N., & Gurevich, Y. (2021). The role of formal methods in ensuring software correctness. Formal Methods for Software Engineering, 29(4), 185–203 c.

Microsoft Research. (2020). Formal verification of cloud services: Case studies and methods. Proceedings of the ACM on Cloud Computing, 11(2), 120–139 c.

Amazon Web Services (AWS). (2021). Using TLA+ for system modeling and verification. AWS Architecture Blog. Retrieved from https://aws.amazon.com/architecture/ Використано в розділі «Впровадження у промислових умовах».

Bjørner, N., & Gurevich, Y. (2021). Using cloud technologies for scalable formal verification. IEEE Transactions on Cloud Computing, 9(7), 412–426 c.

Amazon Web Services. (2021). TLA+: Model checking for cloud systems. Retrieved from https://aws.amazon.com/tla/

Katoen, J., & Baier, C. (2020). Formal verification in DevOps environments: Challenges and potential solutions. International Journal of Software Engineering and Knowledge Engineering, 30(3), 250–271 c..

Ng, B., & Turner, S. (2020). Cloud-based formal verification tools for DevSecOps. ACM Digital Library. Retrieved from https://dl.acm.org/

##submission.downloads##

Опубліковано

2025-02-25