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

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

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

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

Рівень 0

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

Рівень 1

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

Рівень 2

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

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

• VDM
• Z нотація
• B-метод
• Мережа Петрі
• Катастрофа Аріан 5
• OBJ (мова програмування)
• Satisfiability Modulo Theories

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

• 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.

Посилання[ред. | ред. код]

• Віртуальна бібліотека, присвячена формальним методам

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

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