Формальні методи (англ. Formal methods) — у комп'ютерних науках, побудовані на математиці методи написання специфікацій, розробки та перевірки (англ. verification) програмного забезпечення та комп'ютерного обладнання. Цей підхід особливо важливий для вбудованих систем, для яких важливими є надійність або безпека, для захисту від помилок у процесі розробки. Застосування формальних методів особливо ефективне на ранніх етапах написання вимог та специфікацій, але, вони також можуть застосовуватися для повністю формальної розробки реалізації (наприклад, програми).
Таксономія
Формальні методи може бути застосовано на декількох рівнях:
- Рівень 0
- Написання формальної специфікації та неформалізована розробка, на її основі, програмного забезпечення. Такий підхід, також, має назву спрощені формальні методи. Він може бути найоптимальнішим підходом з погляду витрат у багатьох випадках.
- Рівень 1
- Формальний підхід до розробки та перевірки програмного забезпечення може використовуватись для формальнішої реалізації програми. Наприклад, може виконуватись доведення властивостей або уточнення (англ. refinement) із формальної специфікації в програмі. Такий підхід найоптимальніший у вбудованих системах, які повинні мати високий рівень безпеки або надійності.
- Рівень 2
- Можливе застосування систем автоматичного доведення теорем для проведення повністю автоматизованої перевірки доведення теорем. Це може бути занадто дорого, і, на практиці, застосовується у випадках, коли ціна помилок може бути зависокою (наприклад, в критично важливих частинах схеми мікропроцесорів).
Див. також
Література
- Bjorner, Dines. Software Engineering 1: Abstraction and Modelling (Texts in Theoretical Computer Science. An EATCS Series). Springer. ISBN .
- Bjorner, Dines. Software Engineering 2: Specification of Systems and Languages (Texts in Theoretical Computer Science. An EATCS Series). Springer. ISBN .
- Bjorner, Dines. Software Engineering 3: Domains, Requirements, and Software Design (Texts in Theoretical Computer Science. An EATCS Series). Springer. ISBN .
Посилання
![]() | Це незавершена стаття про програмування. Ви можете проєкту, виправивши або дописавши її. |
![]() | Це незавершена стаття з інформатики. Ви можете проєкту, виправивши або дописавши її. |
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
U Vikipediyi ye statti pro inshi znachennya cogo termina Formalnij metod znachennya Formalni metodi angl Formal methods u komp yuternih naukah pobudovani na matematici metodi napisannya specifikacij rozrobki ta perevirki angl verification programnogo zabezpechennya ta komp yuternogo obladnannya Cej pidhid osoblivo vazhlivij dlya vbudovanih sistem dlya yakih vazhlivimi ye nadijnist abo bezpeka dlya zahistu vid pomilok u procesi rozrobki Zastosuvannya formalnih metodiv osoblivo efektivne na rannih etapah napisannya vimog ta specifikacij ale voni takozh mozhut zastosovuvatisya dlya povnistyu formalnoyi rozrobki realizaciyi napriklad programi TaksonomiyaFormalni metodi mozhe buti zastosovano na dekilkoh rivnyah Riven 0 Napisannya formalnoyi specifikaciyi ta neformalizovana rozrobka na yiyi osnovi programnogo zabezpechennya Takij pidhid takozh maye nazvu sprosheni formalni metodi Vin mozhe buti najoptimalnishim pidhodom z poglyadu vitrat u bagatoh vipadkah Riven 1 Formalnij pidhid do rozrobki ta perevirki programnogo zabezpechennya mozhe vikoristovuvatis dlya formalnishoyi realizaciyi programi Napriklad mozhe vikonuvatis dovedennya vlastivostej abo utochnennya angl refinement iz formalnoyi specifikaciyi v programi Takij pidhid najoptimalnishij u vbudovanih sistemah yaki povinni mati visokij riven bezpeki abo nadijnosti Riven 2 Mozhlive zastosuvannya sistem avtomatichnogo dovedennya teorem dlya provedennya povnistyu avtomatizovanoyi perevirki dovedennya teorem Ce mozhe buti zanadto dorogo i na praktici zastosovuyetsya u vipadkah koli cina pomilok mozhe buti zavisokoyu napriklad v kritichno vazhlivih chastinah shemi mikroprocesoriv Div takozhVDM Z notaciya B metod Merezha Petri Katastrofa Arian 5 OBJ mova programuvannya Satisfiability Modulo TheoriesLiteraturaBjorner 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 PosilannyaCe nezavershena stattya pro programuvannya Vi mozhete dopomogti proyektu vipravivshi abo dopisavshi yiyi Ce nezavershena stattya z informatiki Vi mozhete dopomogti proyektu vipravivshi abo dopisavshi yiyi