Методи формальної верифікації програмного забезпечення

Abstract

Бакалаврська робота на тему - Методи формальної верифікації програмного забезпечення. Метою роботи є дослідження методів формальної верифікації програмного забезпечення та аналіз підходів до забезпечення надійності, коректності та безпеки програмних систем. Об’єкт дослідження: процеси розробки та перевірки програмного забезпечення. Предмет дослідження: методи, моделі та інструменти формальної верифікації програмного забезпечення, зокрема математичні методи доведення коректності, формальні специфікації та статичний аналіз. Результати дослідження: проведено аналіз сучасних підходів до формальної верифікації, досліджено класифікацію формальних методів, розглянуто інструментальні засоби їх застосування та оцінено ефективність. У першому розділі розглянуто теоретичні основи формальної верифікації програмного забезпечення, основні поняття, принципи та класифікацію формальних методів. У другому розділі досліджено сучасні методи та інструменти формальної верифікації, включаючи статичний аналіз, формальні специфікації та практичні приклади застосування. У третьому розділі розглянуто реалізацію та оцінку ефективності методів формальної верифікації, проведено аналіз результатів їх застосування та визначено їх вплив на якість програмного забезпечення. Висновок: використання методів формальної верифікації дозволяє значно підвищити надійність, безпеку та коректність програмного забезпечення, зменшити кількість помилок на ранніх етапах розробки.