Верифіка́ція форма́льна — в інформаційних технологіях, доказ, або заперечення відповідності системи у відношенні до певної формальної специфікації або характеристики, із використанням формальних методів математики.
Обґрунтування Редагувати
Тестування програмного забезпечення не може довести, що система, алгоритм або програма не містить ніяких помилок і дефектів та задовольняє певним властивостям. Це може зробити формальна верифікація.
Сфери застосування Редагувати
Формальна верифікація може використовуватися для перевірки таких систем, як програмне забезпечення, представлене у вигляді вихідних текстів, криптографічні протоколи, комбінаторні логічні схеми, цифрові схеми з внутрішньою пам'яттю.
Теоретичні основи Редагувати
Верифікація являє собою формальний доказ на абстрактній математичній моделі системи, в припущенні про те, що відповідність між математичною моделлю і природою системи вважається заданим. Наприклад, щодо побудованої моделі або математичного аналізу, доказ правильності алгоритмів і програм.
Прикладами математичних об'єктів, часто використовуваних для моделювання та формальної верифікації програм і систем, є:
- формальна семантика мов програмування, наприклад операційна семантика, денотаціонная семантика, аксіоматична семантика (Логіка Гоара), [математична семантика програм].
- кінцевий автомат
- позначена модель станів і переходів
- мережа Петрі
- часовий автомат
- гібридний автомат
- числення процесів
- структуровані алгоритми
- структуровані програми
Підходи до формальної верифікації Редагувати
Існують такі підходи до формальної верифікації:
- формальна семантика мов програмування
- перевірка моделей (англ. model checking)
- логічний висновок (англ. logical inference)
- символьне виконання (англ. symbolic execution)
- абстрактна інтерпретація
- систематичний аналіз алгоритмів та програм
- технології доказового програмування
Доказове програмування Редагувати
Доказове програмування - використовувалось в 1980-х роках в академічних колах технології розробки програм для ЕОМ з доказами правильності - доказами відсутності помилок в програмах (розуміючи, в рамках даної теорії, помилки як невідповідності між програмою і реалізованим нею алгоритмом).
Автоматична перевірка доказу Редагувати
Доказ може бути автоматизований повністю лише для дуже невеликого кола простих теорій, тому важливого значення набуває його автоматична перевірка і для цього приведення до належного вигляду.
Для підтримки строгості при перевірці доказу верифікатором слід перевірити ще й верифікатор, для чого потрібен ще один верифікатор і так далі. Отриманий нескінченний ланцюг верифікаторів можна було б згорнути, побудувавши веріфікуючий себе верифікатор, що володіє здатністю розвернутися до застосовного на практиці.
Джерела інформації Редагувати
- Formal verification — стаття в англомовній вікіпедії.
Див. також Редагувати
- Верифікація — споріднений термін із галузі філософії та методології науки.
| Це незавершена стаття про інформаційні технології. Ви можете допомогти проєкту, виправивши або дописавши її. |