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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

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

Обгрунтування[ред.ред. код]

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

Області застосування[ред.ред. код]

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

Теоретичні основи[ред.ред. код]

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

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

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

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

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

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

Доказове програмування[ред.ред. код]

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

Автоматична перевірка доказу[ред.ред. код]

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

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

Джерела інформації[ред.ред. код]

Див. також[ред.ред. код]

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


Комп'ютер Це незавершена стаття про комп'ютери.
Ви можете допомогти проекту, виправивши або дописавши її.