Формальні методи: відмінності між версіями
Перейти до навігації
Перейти до пошуку
| [неперевірена версія] | [неперевірена версія] |
Вилучено вміст Додано вміст
Немає опису редагування |
→Дивіться також: доповнення |
||
| Рядок 14: | Рядок 14: | ||
== Дивіться також == |
== Дивіться також == |
||
*[[Vienna Development Method|VDM]] |
* [[Vienna Development Method|VDM]] |
||
*[[Z нотація]] |
* [[Z нотація]] |
||
*[[Мережа Петрі]] |
* [[Мережа Петрі]] |
||
=== Література === |
|||
| ⚫ | |||
* {{Cite book | author=Bjorner, Dines| title=Software Engineering 1: Abstraction and Modelling (Texts in Theoretical Computer Science. An EATCS Series) | date= | publisher=Springer | location= | isbn=3-540-21149-7}} |
|||
| ⚫ | |||
* {{Cite book | author=Bjorner, Dines | title=Software Engineering 2: Specification of Systems and Languages (Texts in Theoretical Computer Science. An EATCS Series) | date= | publisher=Springer | location= | isbn=3-540-21150-0}} |
|||
* {{Cite book | author=Bjorner, Dines | title=Software Engineering 3: Domains, Requirements, and Software Design (Texts in Theoretical Computer Science. An EATCS Series) | date= | publisher=Springer | location= | isbn=3-540-21151-9}} |
|||
| ⚫ | |||
| ⚫ | |||
{{Compu-stub}} |
{{Compu-stub}} |
||
Версія за 10:33, 13 листопада 2008
Формальні методі (англ. 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.
Ресурси в інтернету
|
Це незавершена стаття про інформаційні технології. Ви можете допомогти проєкту, виправивши або дописавши її. |