Формалне методе

У рачунарству, посебно софтверском инжењерству и хардверском инжењерству, формалне методе су посебна врста математички заснованих техника за спецификацију, развој и верификацију софтвера и хардвера система.^[1] Употреба формалних метода за софтверски и хардверски дизајн је мотивисана очекивањем да, као и у другим инжењерским дисциплинама, обављање одговарајућих математичких анализа може допринети поузданости и робусности дизајна.^[2]

Формалне методе се најбоље описују као примена прилично широког спектра теоријских основа информатике, посебно логике рачунања, формалн ог језика, теорије аутомата, и програмске семантике, али такође типове система и алгебарске структуре података за проблеме у софтверској и хардверској спецификацији и верификацији.^[3]

Таксономија

Формални поступци се могу користити на више нивоа:

Ниво 0: Формална спецификација може се предузети, а затим програм развити од овога неформално. Ово је названо формалне методе лите. Ово може да буде опција најисплативија у многим случајевима.

Ниво 1: Формални развој и формална верификација се могу користити за производњу програма на формалнији начин. На пример, докази о особинама или префињености из спецификације на програм може се предузети. Ово може бити најприкладније у системима високог интегритета који укључују безбедност или сигурност.

Ниво 2: Теорема провере може да се користи да предузме у потпуности формалне доказе машински проверене. Ово може бити веома скупо и само практично исплативо ако је цена грешака изузетно висока (на пример, у критичним деловима микропроцесора дизајна).

Додатне информације о томе су испод проширене.

Као и код семантике програмских језика, стилови формалних метода могу се грубо класификовати на следећи начин:

Денотациона семантика, у којој се смисао система изражава у математичкој теорији домена. Заговорници таквих метода се ослањају на добро разумну природу домена да дају смисао система; критичари истичу сваки систем који не може да се интуитивно или природно прегледа у функцији.
Оперативна семантика, у којој је смисао система изражен као низ акција у (вероватно) једноставнијем израчунавању модела. Заговорници таквих метода указују на једноставност својих модела као средство за изражајне јасноће; критичари одговарају да је проблем семантике управо одложен (који дефинише семантику од једноставнијих модела?).
Аксиом семантика, у којој се смисао система изражава у смислу предуслова и постуслова који су тачни пре и после обављања системског задатка. Заговорници пазе на везу класичне логике; Критичари пазе да никада таква семантика заиста не описује шта систем ради (само оно што је истинито пре и након).

Лагане формалне методе

Неки стручњаци верују да је заједница формалних метода занемарила пуну формализацију спецификације или дизајна.^[4]^[5] Они тврде да експресија језика који су укључени, као и сложеност система који се моделира, даје пуну формализацију тешких и скупих задатака. Као алтернатива, предложене су различите лагане формалне методе, које наглашавају делимичну спецификацију и фокусирану апликацију. Примери овог лаког приступа формалних метода обухватају сплав објеката моделирања записа,^[6] Денијеву синтезу неких аспеката Z ознака са случај коришћења возног развоја,^[7]и ЦСК ВДМ алата.^[8]

Употреба

Формалне методе могу се применити на различитим тачкама у развојном процесу.

Спецификација

Формалне методе се могу користити да дају опис системима да се развијају, на било којем нивоу жељеног детаља. Овај формални опис може да се користи за усмеравање даљег развоја активности (види следеће одељке); Поред тога, може да се користи да провери да ли су захтеви за развијен систем потпуно и тачно назначени.

Потреба за формалном спецификацијом система је истакнута годинама. У извештају ALGOL 58 ,^[9] Џон Бакус представио је формални запис за описивање синтаксе програмског језика (касније названа Бакус нормална форма касније преименована Бакус–Наурова форма (BNF)^[10]). Бакус је такође написао да формални опис значења синтакси важећих Алгол програма није завршена на време за укључивање у извештај. "Стога формални третман семантике правних програма биће укључен у наредном папиру." То се није појавило.

Развој

Када је формална спецификација настала, спецификација је могла да се користи као водич док је бетон систем развијен током процеса пројектовања (нпр, схватио обично у софтверу, али и потенцијално у хардверу). На пример:

Ако је формална спецификација у оперативној семантици, посматрано понашање конкретног система може се упоредити са понашањем спецификације (која је и сама требо да буде извршена). Поред тога, оперативне команде ове спецификације могу бити подложне директном преводу на извршни код.
Ако је формална спецификација у једној аксиоматској семантици, предуслови и послеуслови у спецификацији могу постати тврдње у извршном коду.

Верификација

Када је формална спецификација развијена, спецификација је могла да се користити као основа за доказивање својства спецификације (и надамо се закључивањем развијеног система).

Људски усмерен доказ

Понекад мотивација за доказивање исправности система није очигледна потреба за ре-осигурање исправности система, али је жеља да се боље разумеју системи. Сходно томе, неки докази о коректности су произведени у стилу математичких доказа: у рукопису (или слагала) користећи природни језик, користећи ниво неформалног заједничког таквог доказа. "Добар" доказ је онај који је читљив и разумљив од стране других људских читалаца.

Критичари оваквог приступа истичу да је двосмисленост својствена природном језику и да дозвољава грешке да се нађу непримећено у таквим доказима; Често, суптилне грешке могу бити присутне у детаљима на ниском нивоу обично превиде таквих доказа. Осим тога, рад укључен у израду тако доброг доказа захтева висок ниво математичке софистицираности и стручности.

Аутоматски доказ

Насупрот томе, постоји све веће интересовање у производњи доказа о исправности таквих система и аутоматски начин. Аутоматизоване технике спадају у три категорије:

Аутоматско доказивање теорема, у којем систем покушава да произведе формални доказ од нуле, с обзиром на опис система, скуп логичких аксиома, и скуп правила закључивања.
Провера модела, у којој систем проверава одређене особине помоћу исцрпних потрага за свим могућим земаљама да систем уђе у његово извршење.
Апстрактна интерпретација, у којој систем проверава претерано приближавање неког понашања имовине програма, користећи фикпоинт рачунање преко (евентуално) комплетне решетке га заступа.

Неке аутоматизоване теорема провере захтевају смернице о томе које особине су "занимљиве" да наставе, док други раде без људске интервенције. Модел провере може брзо да вас закочи у провери милион незанимљивих држава, ако не даје довољно апстрактни модел.

Заговорници таквих система тврде да резултати имају већу математичку сигурност од људских произведених доказа, јер сви заморни детаљи су алгоритмички проверени. Потребе тренинга да користи такве системе је такође мање него што је потребно да произведе добре математичке доказе руком, израду технике доступне различитим практичарима.

Критичари имају на уму да неки од тих система су као пророчанстава: праве изрицање истине, али не дају објашњење те истине. Ту је и проблем "провере верификатора"; ако програм који помаже у верификацији сам по себи није доказан, може бити разлог да се сумња у исправност произведених резултата. Неки алати модерног модела провере производе "доказ дневник" детаљно сваки корак у њиховом доказу, тако да је могуће да се изврши, с обзиром на одговарајући алат, независна верификација.

Главна карактеристика апстрактног приступа тумачењу је да пружа добру анализу, односно нема лажи, се вратила. Штавише, то је ефикасно прилагодљиво, подешавање апстрактног домена представља имовину која се анализира, а применом проширења оператера^[11] да се брзо приближава.

Апликације

Формалне методе се примењују у различитим областима хардвера и софтвера, укључујући рутере, екстерне прекидаче, усмеравање протокола и безбедности апликација. Постоји неколико примера у којима су коришћени за проверу функционалности хардвера и софтвера који се користи у DCs. IBM користи ACL2, a теорему провере, у процесу израде AMD x86 процесора. Интел користи такве методе да провери свој хардвер и фирмваре (стални софтвер програмиран у меморија само за читање). Dansk Datamatik Center користи формалне методе у 1980 да развије преводилац систем за Ада програмски језик који је отишао да постане дуговечни комерцијални производ.^[12]^[13]

Постоји неколико других пројеката НАСЕ у којима се примењују формалне методе, као што је Следећа генерација ваздушног транспортног система, Unmanned Aircraft System integration in National Airspace System,^[14] и Airborne Coordinated Conflict Resolution and Detection (ACCoRD).^[15] B-Method са AtelierB,^[16] се користи за развој безбедности аутоматизама за разне метрое инсталиране широм света од стране Alstom и Siemens, као и за заједничке критеријуме сертификаце и развој модела система од ATMEL и STMicroelectronics.

Формална верификација је често коришћена у хардверу већине познатих хардвера, као што су IBM, Интел, и АМД. Постоје многе области хардвера, где Интел користии ФМС да провери функционисање производа, као што су параметризована верификација кеша кохерентност протокола,^[17] Intel Core i7 процесор валидација извршења мотора ^[18] (користећи доказивање теорема, BDD’s, и симболичку евалуацију), оптимизација за Intel IA-64 архитектуру користећи ХОЛ светло теорему провере,^[19] и верификација високих перформанси дуал-порт екстерни контролер са подршком за ПС експрес протокол и Интел напредну технологију за управљање помоћу ритма.^[20] Слично томе, IBM је користио формалне методе у верификацији моћи капије,^[21] регистри,^[22] и функционална верификација IBM Power7 микропроцесора.^[23]

Формалне методе и ознаке

Постоји низ формалних метода и ознака на располагању.

Спецификација језика

Модели провере

SPIN
Пат је моћан бесплатан модел провере, симулатор и префињен модел провере за истовремене системе и СПРС локале (нпр заједничке варијабле, низови, правичност).
MALPAS Software Static Analysis Toolset је индустријски снажни модел провере који се користи за формални доказ о сигурности критичних система
UPPAAL

Види још

Референце

^ R. W. Butler (6. 8. 2001). „What is Formal Methods?”. Приступљено 16. 11. 2006.
^ C. Michael Holloway. „Why Engineers Should Consider Formal Methods” (PDF). 16th Digital Avionics Systems Conference (27–30 October 1997). Архивирано из оригинала 06. 06. 2012. г. Приступљено 16. 11. 2006.
^ Monin, стр. 3–4
^ Daniel Jackson and Jeannette Wing, "Lightweight Formal Methods", IEEE Computer, April 1996
^ Vinu George and Rayford Vaughn, archive "Application of Lightweight Formal Methods in Requirement Engineering", Crosstalk: The Journal of Defense Software Engineering, January 2003
^ Daniel Jackson, (4. 2002). „"Alloy: A Lightweight Object Modelling Notation"” (PDF). ACM Transactions on Software Engineering and Methodology (TOSEM). 11 (2). . стр. 256—290
^ Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality, Addison-Wesley Professional Publishing. 2005. ISBN 0-321-31643-6
^ Sten Agerholm and Peter G. Larsen, archive "A Lightweight Approach to Formal Methods", In Proceedings of the International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, Springer-Verlag, October 1998
^ Backus, J.W. (1959). „The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference”. Proceedings of the International Conference on Information Processing. UNESCO.
^ Knuth, Donald E. (1964), Backus Normal Form vs Backus Naur Form.
^ A.Cortesi and M.Zanioli, Widening and Narrowing Operators for Abstract Interpretation Архивирано на веб-сајту Wayback Machine (23. септембар 2015).
^ Bjørner et al. 2011, стр. 350–359
^ Bjørner, Dines; Havelund, Klaus. „40 Years of Formal Methods: Some Obstacles and Some Possibilities?”. FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12–16, 2014. Proceedings. Springer. стр. 42—61.
^ Gheorghe, A. V., & Ancel, E. (2008, November).
^ Airborne Coordinated Conflict Resolution and Detection, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/ Архивирано на веб-сајту Wayback Machine (5. март 2016)
^ website : http://www.atelierb.eu/en/ Архивирано на веб-сајту Wayback Machine (13. јануар 2016)
^ C. T. Chou, P. K. Mannava, S. Park, “A simple method for parameterized verification of cache coherence protocols,” Formal Methods in Computer-Aided Design. стр. 382-398, 2004.
^ Formal Verification in Intel® Core™ i7 Processor Execution Engine Validation, http://cps-vo.org/node/1371 Архивирано на веб-сајту Wayback Machine (3. мај 2015), accessed at Sep. 13, 2013.
^ J. Grundy, “Verified optimizations for the Intel IA-64 architecture,” In Theorem Proving in Higher Order Logics, Springer Berlin Heidelberg. (2004). стр. 215—232.
^ E. Seligman, I. Yarom, “Best known methods for using Cadence Conformal LEC,” at Intel.
^ C. Eisner, A. Nahir, K. Yorav, “Functional verification of power gated designs by compositional reasoning,” Computer Aided Verification Springer Berlin Heidelberg. стр. 433-445.
^ P. C. Attie, H. Chockler, “Automatic verification of fault-tolerant register emulations,” Electronic Notes in Theoretical Computer Science, 149 (1): 49–60.
^ K. D. Schubert, W. Roesner, J. M. Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, “Functional verification of the IBM POWER7 microprocessor and POWER7 multiprocessor systems,” IBM Journal of Research and Development, 55 (3):.

Литература

Овај чланак је заснован на материјалу преузетом из Free On-line Dictionary of Computing до 1. новембра 2008. године и уграђен је под "релиценцирањем" под GFDL, верзија 1.3 или новије.
Jean François Monin; Hinchey, Michael G. (2003). Understanding formal methods. Springer. ISBN 1-85233-247-6.
Jonathan P. Bowen and Michael G. Hinchey, Formal Methods. In Allen B. Tucker, Jr. (ed.), Computer Science Handbook, 2nd edition, Section XI, Software Engineering,Chapter 106, pages 106-1 – 106-25, Chapman & Hall / CRC Press, Association for Computing Machinery, 2004.
Michael G. Hinchey, Jonathan P. Bowen, and Emil Vassev, Formal Methods. In Philip A. Laplante (ed.), Encyclopedia of Software Engineering, Taylor & Francis, 2010, pages 308–320.
Bjørner, Dines; Gram, Christian; Oest, Ole N.; Rystrøm, Leif (2011). „Dansk Datamatik Center”. Ур.: Impagliazzo, John; Lundin, Per; Wangler, Benkt. History of Nordic Computing 3: IFIP Advances in Information and Communication Technology. Springer. стр. 350—359.