Формальна верифікація

Форма́льна верифіка́ція — в інформаційних технологіях, доведення, або заперечення відповідності системи певній формальній специфікації або характеристиці, із використанням формальних методів математики.

Обґрунтування

Тестування програмного забезпечення не може довести, що система, алгоритм або програма не містить ніяких помилок і дефектів та задовольняє певним властивостям. Це може зробити формальна верифікація.

Сфери застосування

Формальна верифікація може використовуватися для перевірки таких систем, як програмне забезпечення, представлене у вигляді вихідних текстів, криптографічні протоколи, комбінаторні логічні схеми, цифрові схеми з внутрішньою пам'яттю.

Теоретичні основи

Верифікація являє собою формальне доведення на абстрактній математичній моделі системи, в припущенні про те, що відповідність між математичною моделлю і природою системи вважається заданим. Наприклад, щодо побудованої моделі або математичного аналізу, доведення правильності алгоритмів і програм.

Прикладами математичних об'єктів, часто використовуваних для моделювання та формальної верифікації програм і систем, є:

• формальна семантика мов програмування, наприклад операційна семантика, денотаційна семантика, аксіоматична семантика (Логіка Гоара), математична семантика програм.
• кінцевий автомат
• позначена модель станів і переходів
• мережа Петрі
• часовий автомат
• гібридний автомат
• числення процесів
• структуровані алгоритми
• структуровані програми

Підходи до формальної верифікації

Існують такі підходи до формальної верифікації:

• формальна семантика мов програмування
• перевірка моделей (англ. model checking)
• логічний висновок (англ. logical inference)
• символьне виконання (англ. symbolic execution)
• абстрактна інтерпретація
• систематичний аналіз алгоритмів та програм
• технології доказового програмування

Доказове програмування

Доказове програмування - використовувалось в 1980-х роках в академічних колах технології розробки програм для ЕОМ з доведеннями правильності - доведенням відсутності помилок у програмах (розуміючи, в рамках даної теорії, помилки як невідповідності між програмою і реалізованим нею алгоритмом).

Автоматична перевірка доведення

Доведення можна автоматизувати повністю лише для дуже невеликого кола простих теорій, тому зростає важливість його автоматичної перевірки і для цього зведення до належного вигляду.

Для підтримки строгості при перевірці доведення верифікатором слід перевірити ще й верифікатор, для чого потрібен ще один верифікатор і так далі. Отриманий нескінченний ланцюг верифікаторів можна було б згорнути, побудувавши самоверифіковний верифікатор, що володіє здатністю розвернутися до застосовного на практиці.

Див. також

• Верифікація — споріднений термін із галузі філософії та методології науки.
• SPARK (мова програмування)