Формальні методи програмування

Формальні методі (англ. Formal methods) — в комп'ютерних науках, основані на математиці методи написання специфікацій, розробки та верифікації (перевірки) програмного забезпечення (ПЗ) та комп'ютерного обладнання. Цей підхід особливо важливий для вбудованих систем, для яких важливими є надійність або безпека, для захисту від появи помилок в процесі розробки. Застосування формальних методів особливо ефективно на ранніх етапах написання вимог та специфікацій, але, також, можуть використовуватись для повністю формальної розробки реалізації (наприклад, програми). Існують стандарти на критерії безпечності та захищенності программ. Частіше за все для реалізації валідації ПЗ використовуються теорія скінчених автоматів.

Формальні методи можуть бути застосовані на декількох рівнях:

Рівень 0

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

Рівень 1

Формальний підхід до розробки програмного забезпечення та перевірки може використовуватись для формальнішої реалізації програми. Наприклад, може виконуватись доведення властивостей або уточнення (англ. refinement) із формальної специфікації в програмі. Такий підхід найоптимальніший у вбудованих системах, які повинні мати високий рівень безпеки або надійності.

Рівень 2

Можливе застосування систем автоматичного доведення теорем для проведення повністю автоматизованої перевірки доведення теорем. Це може бути занадто дорого, і, на практиці, застосовується у випадках, коли ціна помилок може бути зависокою (наприклад, в критично важливих частинах схеми мікропроцесорів).

Відомі формальні методи: Event-B, Z-notation, ASM, RAISE, SLAM, Мережі Петрі та ін.

Теорія програмування та обчислень