Форма́льна верифіка́ція — в інформаційних технологіях, доведення, або заперечення відповідності системи певній формальній специфікації або характеристиці, із використанням формальних методів математики.
Обґрунтування
Тестування програмного забезпечення не може довести, що система, алгоритм або програма не містить ніяких помилок і дефектів та задовольняє певним властивостям. Це може зробити формальна верифікація.
Сфери застосування
Формальна верифікація може використовуватися для перевірки таких систем, як програмне забезпечення, представлене у вигляді вихідних текстів, криптографічні протоколи, комбінаторні логічні схеми, цифрові схеми з внутрішньою пам'яттю.
Теоретичні основи
Верифікація являє собою формальне доведення на абстрактній математичній моделі системи, в припущенні про те, що відповідність між математичною моделлю і природою системи вважається заданим. Наприклад, щодо побудованої моделі або математичного аналізу, доведення правильності алгоритмів і програм.
Прикладами математичних об'єктів, часто використовуваних для моделювання та формальної верифікації програм і систем, є:
- формальна семантика мов програмування, наприклад операційна семантика, денотаційна семантика, аксіоматична семантика (Логіка Гоара), .
- кінцевий автомат
- позначена модель станів і переходів
- мережа Петрі
- часовий автомат
- гібридний автомат
- числення процесів
- структуровані алгоритми
- структуровані програми
Підходи до формальної верифікації
Існують такі підходи до формальної верифікації:
- формальна семантика мов програмування
- перевірка моделей (англ. model checking)
- логічний висновок (англ. logical inference)
- символьне виконання (англ. symbolic execution)
- абстрактна інтерпретація
- систематичний аналіз алгоритмів та програм
- технології доказового програмування
Доказове програмування
Доказове програмування - використовувалось в 1980-х роках в академічних колах технології розробки програм для ЕОМ з доведеннями правильності - доведенням відсутності помилок у програмах (розуміючи, в рамках даної теорії, помилки як невідповідності між програмою і реалізованим нею алгоритмом).
Автоматична перевірка доведення
Доведення можна автоматизувати повністю лише для дуже невеликого кола простих теорій, тому зростає важливість його автоматичної перевірки і для цього зведення до належного вигляду.
Для підтримки строгості при перевірці доведення верифікатором слід перевірити ще й верифікатор, для чого потрібен ще один верифікатор і так далі. Отриманий нескінченний ланцюг верифікаторів можна було б згорнути, побудувавши самоверифіковний верифікатор, що володіє здатністю розвернутися до застосовного на практиці.
Див. також
- Верифікація — споріднений термін із галузі філософії та методології науки.
- SPARK (мова програмування)
Примітки
- Sanghavi, Alok (21 травня 2010). What is formal verification?. EE Times Asia.
- Introduction to Formal Verification, Berkeley University of California, Retrieved November 6, 2013
![]() | Це незавершена стаття про інформаційні технології. Ви можете проєкту, виправивши або дописавши її. |
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, 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 Verifikaciya znachennya Forma lna verifika ciya v informacijnih tehnologiyah dovedennya abo zaperechennya vidpovidnosti sistemi pevnij formalnij specifikaciyi abo harakteristici iz vikoristannyam formalnih metodiv matematiki ObgruntuvannyaTestuvannya programnogo zabezpechennya ne mozhe dovesti sho sistema algoritm abo programa ne mistit niyakih pomilok i defektiv ta zadovolnyaye pevnim vlastivostyam Ce mozhe zrobiti formalna verifikaciya Sferi zastosuvannyaFormalna verifikaciya mozhe vikoristovuvatisya dlya perevirki takih sistem yak programne zabezpechennya predstavlene u viglyadi vihidnih tekstiv kriptografichni protokoli kombinatorni logichni shemi cifrovi shemi z vnutrishnoyu pam yattyu Teoretichni osnoviVerifikaciya yavlyaye soboyu formalne dovedennya na abstraktnij matematichnij modeli sistemi v pripushenni pro te sho vidpovidnist mizh matematichnoyu modellyu i prirodoyu sistemi vvazhayetsya zadanim Napriklad shodo pobudovanoyi modeli abo matematichnogo analizu dovedennya pravilnosti algoritmiv i program Prikladami matematichnih ob yektiv chasto vikoristovuvanih dlya modelyuvannya ta formalnoyi verifikaciyi program i sistem ye formalna semantika mov programuvannya napriklad operacijna semantika denotacijna semantika aksiomatichna semantika Logika Goara kincevij avtomat poznachena model staniv i perehodiv merezha Petri chasovij avtomat gibridnij avtomat chislennya procesiv strukturovani algoritmi strukturovani programiPidhodi do formalnoyi verifikaciyiIsnuyut taki pidhodi do formalnoyi verifikaciyi formalna semantika mov programuvannya perevirka modelej angl model checking logichnij visnovok angl logical inference simvolne vikonannya angl symbolic execution abstraktna interpretaciya sistematichnij analiz algoritmiv ta program tehnologiyi dokazovogo programuvannyaDokazove programuvannyaDokazove programuvannya vikoristovuvalos v 1980 h rokah v akademichnih kolah tehnologiyi rozrobki program dlya EOM z dovedennyami pravilnosti dovedennyam vidsutnosti pomilok u programah rozumiyuchi v ramkah danoyi teoriyi pomilki yak nevidpovidnosti mizh programoyu i realizovanim neyu algoritmom Avtomatichna perevirka dovedennyaDovedennya mozhna avtomatizuvati povnistyu lishe dlya duzhe nevelikogo kola prostih teorij tomu zrostaye vazhlivist jogo avtomatichnoyi perevirki i dlya cogo zvedennya do nalezhnogo viglyadu Dlya pidtrimki strogosti pri perevirci dovedennya verifikatorom slid pereviriti she j verifikator dlya chogo potriben she odin verifikator i tak dali Otrimanij neskinchennij lancyug verifikatoriv mozhna bulo b zgornuti pobuduvavshi samoverifikovnij verifikator sho volodiye zdatnistyu rozvernutisya do zastosovnogo na praktici Div takozhVerifikaciya sporidnenij termin iz galuzi filosofiyi ta metodologiyi nauki SPARK mova programuvannya PrimitkiSanghavi Alok 21 travnya 2010 What is formal verification EE Times Asia Introduction to Formal Verification Berkeley University of California Retrieved November 6 2013 Ce nezavershena stattya pro informacijni tehnologiyi Vi mozhete dopomogti proyektu vipravivshi abo dopisavshi yiyi