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

У Вікіпедії є статті про інші значення цього терміна: Верифікація (значення).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Див. також

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