Формальні методи
Матеріал з Вікіпедії — вільної енциклопедії.
Формальні методі (англ. Formal methods) — в комп'ютерних науках, основані на математиці методи написання специфікацій, розробки та перевірки (англ. verification) програмного забезпечення та комп'ютерного обладнання. Цей підхід особливо важливий для вбудованих систем, для яких важливими є надійність або безпека, для захисту від появи помилок в процесі розробки. Застосування формальних методів особливо ефективно на ранніх етапах написання вимог та специфікацій, але, також, можуть використовуватись для повністю формальної розробки реалізації (наприклад, програми).
Зміст |
[ред.] Таксономія
Формальні методи може бути застосовано на декількох рівнях:
- Рівень 0
- Написання формальної специфікації та неформалізована розробка, на її основі, програмного забезпечення. Такий підхід, також, має назву спрощені формальні методи. Він може бути найоптимальнішим, з точки зору витрат, підходом у багатьох випадках.
- Рівень 1
- Формальний підхід до розробки програмного забезпечення та перевірки може використовуватись для формальнішої реалізації програми. Наприклад, може виконуватись доведення властивостей або уточнення (англ. refinement) із формальної специфікації в програмі. Такий підхід найоптимальніший у вбудованих системах, які повинні мати високий рівень безпеки або надійності.
- Рівень 2
- Можливе застосування систем автоматичного доведення теорем для проведення повністю автоматизованої перевірки доведення теорем. Це може бути занадто дорого, і, на практиці, застосовується у випадках, коли ціна помилок може бути зависокою (наприклад, в критично важливих частинах схеми мікропроцесорів).
[ред.] Джерела інформації
- Formal methods — сторінка в анломовній вікіпедії.
[ред.] Дивіться також
[ред.] Ресурси в інтернет
| Це незавершена стаття про комп'ютери. Ви можете допомогти проекту, виправивши або дописавши її. |

