Формальні методи

Матеріал з Вікіпедії — вільної енциклопедії.

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

Зміст

[ред.] Таксономія

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

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

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

  • Formal methods — сторінка в анломовній вікіпедії.

[ред.] Дивіться також

[ред.] Ресурси в інтернет


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