ПРОГРАМА РОЗРІШУВАЧІВ SMT ДЛЯ ФОРМАЛЬНОЇ ПЕРЕВІРКИ СЕРВІСІВ НА ОСНОВІ ПОЛІТИКИ В ХМАРНОМУ СЕРЕДОВИЩІ
DOI:
https://doi.org/10.34185/1991-7848.itmm.2023.01.074Ключові слова:
SMT, автоматизоване міркування, хмарні технології, формальна перевіркаАнотація
Формальна перевірка служб на основі політики в хмарних середовищах за допомогою розв’язувачів SMT (Satisfiability Modulo Theories) передбачає кодування політик і поведінки служб у вигляді логічних формул і перевірку, чи є формули задовільними чи незадовільними. Вирішувачі SMT можна використовувати для перевірки правильності виконання політик і відповідності поведінки служби політикам.
Посилання
Zhang, X., Sun, M. (2019). SMT-Based Modeling and Verification of Cloud Applications. In: Xia, Y., Zhang, LJ. (eds) Services – SERVICES 2019. SERVICES 2019. Lecture Notes in Computer Science(), vol 11517. Springer, Cham.
L. de Moura and N. Bjørner, “Z3: An efficient SMT solver,” Tools and Algorithms for the Construction and Analysis of Systems, pp. 337–340, 2008.
