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

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

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

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

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

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

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

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

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

Література[ред.ред. код]

  • Bjorner, Dines. Software Engineering 1: Abstraction and Modelling (Texts in Theoretical Computer Science. An EATCS Series). Springer. ISBN 3-540-21149-7. 
  • Bjorner, Dines. Software Engineering 2: Specification of Systems and Languages (Texts in Theoretical Computer Science. An EATCS Series). Springer. ISBN 3-540-21150-0. 
  • Bjorner, Dines. Software Engineering 3: Domains, Requirements, and Software Design (Texts in Theoretical Computer Science. An EATCS Series). Springer. ISBN 3-540-21151-9. 

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


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