У Вікіпедії є статті про інші значення цього терміна Формальний метод значення Формальні методи англ Formal methods у ко

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

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

Таксономія

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

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

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

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

Див. також

Література

Bjorner, Dines. Software Engineering 1: Abstraction and Modelling (Texts in Theoretical Computer Science. An EATCS Series). Springer. ISBN .
Bjorner, Dines. Software Engineering 2: Specification of Systems and Languages (Texts in Theoretical Computer Science. An EATCS Series). Springer. ISBN .
Bjorner, Dines. Software Engineering 3: Domains, Requirements, and Software Design (Texts in Theoretical Computer Science. An EATCS Series). Springer. ISBN .

Посилання

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

Це незавершена стаття з інформатики.
Ви можете проєкту, виправивши або дописавши її.