国家卫生计生委办公厅关于成立国家卫生计生...
У контексту хардверских и софтверских система, формална верификаци?а представ?а чин доказива?а или оспорава?а исправности система у односу на одре?ену формалну спецификаци?у или сво?ство, кориш?е?ем формалних математичких метода.[1] Формална верификаци?а ?е к?учни подстица? за формалну спецификаци?у система и налази се у ?езгру формалних метода. Она представ?а важну димензи?у анализе и верификаци?е у аутоматизаци?и електронског диза?на и ?едан ?е од приступа верификаци?и софтвера. Употреба формалне верификаци?е омогу?ава на?виши ниво процене (EAL7) у оквиру за?едничких критери?ума за сертификаци?у рачунарске безбедности.
Формална верификаци?а може бити корисна у доказива?у исправности система као што су: криптографски протоколи, комбинациона кола, дигитална кола са унутраш?ом мемори?ом и софтвер изражен као изворни код у програмском ?езику. Знача?ни примери верификованих софтверских система ук?учу?у верификовани C компа?лер CompCert и ?езгро оперативног система са високим нивоом поузданости seL4.
Верификаци?а ових система се спроводи обезбе?ива?ем посто?а?а формалног доказа математичког модела система.[2] Примери математичких об?еката ко?и се користе за моделира?е система ук?учу?у: коначни аутомат, означене прелазне системе, Хорнове клаузуле, Петри?еве мреже, системе сабира?а вектора, временске аутомате, хибридне аутомате, процесну алгебру, формалну семантику програмских ?езика као што су операциона семантика, денотациона семантика, аксиоматска семантика и Хорова логика.[3]
Приступи
[уреди | уреди извор]?едан од приступа и формаци?а ?е провера модела, ко?а се састо?и од систематски исцрпне експлораци?е математичког модела (ово ?е могу?е за коначне моделе, али и за неке бесконачне моделе где се бесконачни скупови ста?а могу ефективно представити коначно кориш?е?ем апстракци?е или искориш?ава?ем симетри?е). Обично се то састо?и у истражива?у свих ста?а и прелаза у моделу, кориш?е?ем паметних и домен-специфичних техника апстракци?е како би се разматрале целе групе ста?а у ?едно? операци?и и сма?ило време рачуна?а. Технике имплементаци?е ук?учу?у нумераци?у просторa ста?а, симболичку нумераци?у простора ста?а, апстрактну интерпретаци?у, симболичку симулаци?у, и рафинаци?у апстракци?е. Сво?ства ко?а треба верификовати често се опису?у у темпоралним логикама, као што су линеарна темпорална логика (LTL), ?език за спецификаци?у сво?става (PSL), SystemVerilog Assertions (SVA),[4] или комп?утерска логика стабала (CTL). Велика предност провере модела ?е што ?е често потпуно аутоматска; ?ен главни недостатак ?е што се углавном не скалира добро на велике системе; симболички модели су обично ограничени на неколико стотина битова ста?а, док експлицитна нумераци?а ста?а захтева да простор ста?а ко?и се истражу?е буде релативно мали.
Други приступ ?е дедуктивна верификаци?а. Она се састо?и од генериса?а скупа математичких доказних обавеза из система и ?егових спецификаци?а (и могу?их других анотаци?а), чи?а истинитост имплицира ускла?еност система са ?еговом спецификаци?ом, и решава?а тих обавеза кориш?е?ем асистената за доказива?е (интерактивних теорема доказивача), као што су HOL, ACL2, Isabelle, Coq или PVS, или аутоматских доказивача теорема, ук?учу?у?и посебно решаваче задово?ивости модуло теори?а (SMT). Недостатак овог приступа ?е што може захтевати од корисника да дета?но разуме зашто систем ради исправно и да ту информаци?у пренесе систему за верификаци?у, било у облику низа теорема ко?е треба доказати, или у облику спецификаци?а (инвари?анти, предуслови, постуслови) компоненти система (нпр. функци?а или процедура), а можда и поткомпоненти (као што су пет?е или структуре података).
Софтвер
[уреди | уреди извор]Формална верификаци?а софтверских програма подразумева доказива?е да програм задово?ава формалну спецификаци?у свог понаша?а. Подобласти формалне верификаци?е ук?учу?у дедуктивну верификаци?у (види горе), апстрактну интерпретаци?у, аутоматизовано доказива?е теорема, типске системе и лаке формалне методе. ?едан обе?ава?у?и приступ верификаци?и заснован на типовима ?е програмира?е са зависним типовима, у коме типови функци?а ук?учу?у (барем делимично) спецификаци?е тих функци?а, а проверава?е типова кода утвр?у?е ?егову исправност у односу на те спецификаци?е. ?езици са потпуним подршком за зависно типизира?е омогу?ава?у дедуктивну верификаци?у као посебан случа?.
?ош ?едан допунски приступ ?е изво?е?е програма, где се ефикасан код производи из функционалних спецификаци?а кроз сери?у корака ко?и очувава?у исправност. Пример овог приступа ?е Бирд-Мертенсова формализаци?а, и ова? приступ се може сматрати другом формом исправности кроз конструкци?у.
Ове технике могу бити звучне, што значи да се верификована сво?ства могу логички извести из семантике, или незвучне, што значи да нема такве гаранци?е. Звучна техника да?е резултат тек када ?е обухватила цео простор могу?ности. Пример незвучне технике ?е она ко?а покрива само подскуп могу?ности, на пример само целе бро?еве до одре?еног бро?а, и да?е ?дово?но добар“ резултат. Технике тако?е могу бити одлучиве, што значи да су ?ихове алгоритамске имплементаци?е гаранту?у да ?е се завршити са одговором, или неодлучиве, што значи да можда никада не?е завршити. Ограничава?ем обима могу?ности могу?е ?е конструисати незвучне технике ко?е су одлучиве када звучне технике ко?е су одлучиве нису доступне.
Верификаци?а и валидаци?а
[уреди | уреди извор]Верификаци?а ?е ?едан аспект тестира?а подобности производа за ?егову сврху. Валидаци?а ?е комплементарни аспект. Често се цео процес провере назива V & V (верификаци?а и валидаци?а).
- Валидаци?а: "Да ли покушавамо да направимо праву ствар?", односно, да ли ?е производ спецификован у складу са стварним потребама корисника?
- Верификаци?а: "Да ли смо направили оно што смо покушавали да направимо?", т?. да ли производ одговара спецификаци?ама?
Процес верификаци?е се састо?и од статичких/структурних и динамичких/понаша?них аспеката. На пример, за софтверски производ може се прегледати изворни код (статички) и извршити тестира?е против специфичних тест случа?ева (динамички). Валидаци?а се обично може извршити само динамички, т?. производ се тестира став?а?ем у типичне и атипичне сценари?е употребе ("Да ли задово?ава све случа?еве употребе?").
Аутоматизована поправка програма
[уреди | уреди извор]Поправка програма се изводи у складу са "ораклом", што представ?а же?ену функционалност програма ко?а се користи за валидаци?у генерисаних исправки. ?едан ?едноставан пример ?е тест-скуп — парови улаз/излаз дефинишу функционалност програма. Разне технике се користе, на?знача?ни?е ук?учу?у?и решаваче задово?ивости модуло теори?а (SMT) и генетичко програмира?е,[5] ко?е користи еволуциону рачунарску методу за генериса?е и оцену могу?их кандидата за исправке. Први метод ?е детерминистички, док ?е други случа?ан.
Поправка програма комбину?е технике формалне верификаци?е и синтезе програма. Технике локализаци?е грешака у формално? верификаци?и користе се за одре?ива?е тачака у програму ко?е могу бити могу?а места грешака, ко?а могу бити мета модула за синтезу. Системи за поправку често се фокусира?у на малу предефинисану класу грешака како би сма?или простор претраге. Индустри?ска употреба ?е ограничена због рачунарских трошкова посто?е?их техника.
Кориш?е?е у индустри?и
[уреди | уреди извор]Раст комплексности диза?на пове?ава знача? формалних верификационих техника у индустри?и хардвера.[6][7] Тренутно, формална верификаци?а се користи од стране ве?ине или свих воде?их компани?а у области хардвера,[8] али ?ена примена у индустри?и софтвера и да?е ?е ограничена. Ово се може приписати ве?о? потреби у индустри?и хардвера, где грешке има?у ве?е комерци?алне последице. Због потенци?алних суптилних интеракци?а изме?у компоненти, све ?е теже обухватити реалан скуп могу?ности симулаци?ом. Важни аспекти диза?на хардвера су погодни за аутоматизоване методе доказива?а, што чини формалну верификаци?у лакшом за уво?е?е и продуктивни?ом.[9]
До 2011. године, неколико оперативних система ?е формално верификовано: NICTA-ов Secure Embedded L4 микро?езгро, продаван комерци?ално као seL4 од стране OK Labs; [10]OSEK/VDX базирани реално-временски оперативни систем ORIENTAIS са East China Normal University универзитета; оперативни систем Integrity компани?е Green Hills Software; и PikeOS компани?е SYSGO.[11] [12]У 2016. години, тим ко?и ?е предводио Zhong Shao на Универзитету ?е?л развио ?е формално верификовано оперативно ?езгро под називом CertiKOS.[13][14]
До 2017. године, формална верификаци?а ?е приме?ена на диза?н великих рачунарских мрежа путем математичког модела мреже [15] и као део нове категори?е технологи?а мрежа, мрежа заснованих на намерама. [16] Прова?дери софтвера за мреже ко?и нуде реше?а за формалну верификаци?у ук?учу?у Cisco, [17] Forward Networks[18][19] и Veriflow Systems. [20]
Програмски ?език SPARK пружа алате ко?и омогу?ава?у разво? софтвера уз формалну верификаци?у и користи се у неколико система високог интегритета.
Компилатор CompCert C ?е формално верификовани C компилатор ко?и имплементира ве?ину ISO C стандарда. [21][22]
Види тако?е
[уреди | уреди извор]- Аутоматизовано доказива?е теорема
- Провера модела
- Списак алата за проверу модела
- Формална провера ?еднакости
- Провера доказа
- ?език спецификаци?е сво?става
- Статичка анализа кода
- Темпорална логика у верификаци?и коначних ста?а
- Пост-силиконска валидаци?а
- Интелигентна верификаци?а
- Верификаци?а у време изврше?а
Референце
[уреди | уреди извор]- ^ Sanghavi, Alok (21. 5. 2010). ?What is formal verification?”. EE Times Asia.
- ^ Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick, ур. (2018). Handbook of Model Checking (на ?езику: енглески). Cham: Springer International Publishing. ISBN 978-3-319-10574-1.
- ^ ?Introduction to Formal Verification”. ptolemy.berkeley.edu. Приступ?ено 2025-08-07.
- ^ Winikoff, M. (2010), Assurance of Agent Systems: What Role Should Formal Verification Play?, Springer US, стр. 353—383, ISBN 978-1-4419-6983-5, Приступ?ено 2025-08-07
- ^ Le Goues, Claire; Nguyen, ThanhVu; Forrest, Stephanie; Weimer, Westley. ?GenProg: A Generic Method for Automatic Software Repair”. IEEE Transactions on Software Engineering. 38 (1): 54—72. ISSN 0098-5589.
- ^ Harrison, J. (2003). ?Formal verification at Intel”. IEEE Comput. Soc: 45—54. ISBN 978-0-7695-1884-8. doi:10.1109/LICS.2003.1210044.
- ^ Umrigar, Z.D.; Pitchumani, V. (1983). ?Formal Verification of a Real-Time Hardware Design”. 20th Design Automation Conference Proceedings. IEEE. 19: 221—227. doi:10.1109/dac.1983.1585652.
- ^ Seligman, Erik; Schubert, Tom; Kumar, M V Achutha Kiran (2015), Formal verification, Elsevier, стр. 1—22, ISBN 978-0-12-800727-3, Приступ?ено 2025-08-07
- ^ Hunt, James J. (2012), The Practical Application of Formal Methods: Where Is the Benefit for Industry?, Springer Berlin Heidelberg, стр. 22—32, ISBN 978-3-642-31761-3, Приступ?ено 2025-08-07
- ^ ?Original PDF”. dx.doi.org. Приступ?ено 2025-08-07.
- ^ Baumann, Christoph; Beckert, Bernhard; Blasum, Holger; Bormer, Thorsten (2025-08-07). ?Lessons Learned From Microkernel Verification — Specification is the New Bottleneck”. Electronic Proceedings in Theoretical Computer Science. 102: 18—32. ISSN 2075-2180. doi:10.4204/eptcs.102.4.
- ^ Ganssle, Jack G. (2000), Real Time Means Right Now!, Elsevier, стр. 53—85, ISBN 978-0-7506-9869-6, Приступ?ено 2025-08-07
- ^ Harris, Robin (David Ronald), (born 22 June 1952), writer, Oxford University Press, 2025-08-07, Приступ?ено 2025-08-07
- ^ Gold, Steve. ?German firm develops world's first “Trojan-proof” password system”. Infosecurity. 5 (7): 8. ISSN 1754-4548. doi:10.1016/s1754-4548(08)70112-8.
- ^ Beshley, Mykola; Klymash, Mykhailo; Beshley, Halyna; Urikova, Oksana; Bobalo, Yuriy (2025-08-07), Future Intent-Based Networking for QoE-Driven Business Models, Springer International Publishing, стр. 1—18, ISBN 978-3-030-92433-1, Приступ?ено 2025-08-07
- ^ Tsuzaki, Yoshiharu; Okabe, Yasuo (2017). ?Reactive configuration updating for Intent-Based Networking”. 2017 International Conference on Information Networking (ICOIN). IEEE. 15: 97—102. doi:10.1109/icoin.2017.7899484.
- ^ Ao, Weng Chon; Psounis, Konstantinos. ?Data-Locality-Aware User Grouping in Cloud Radio Access Networks”. IEEE Transactions on Wireless Communications. 17 (11): 7295—7308. ISSN 1536-1276. doi:10.1109/twc.2018.2866055.
- ^ RAND Review: January-February 2018. RAND Corporation. 2018.
- ^ Getting in: Data collection in grounded theory, SAGE Publications Ltd, 2018, стр. 31—48, Приступ?ено 2025-08-07
- ^ CROWN-PRINCE RETRIEVED: LIFE AT CUSTRIN NOVEMBER 1730-FEBRUARY 1732, Cambridge University Press, 2025-08-07, стр. 342—406, Приступ?ено 2025-08-07
- ^ Separation logic for CompCert, Cambridge University Press, 2025-08-07, стр. 141—141, Приступ?ено 2025-08-07
- ^ Barrière, Aurèle; Blazy, Sandrine; Pichardie, David (2025-08-07). ?Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler”. Proceedings of the ACM on Programming Languages (на ?езику: енглески). 7 (POPL): 249—277. ISSN 2475-1421. doi:10.1145/3571202.