Википедија

Formalne metode

U računarstvu, posebno softverskom inženjerstvu i hardverskom inženjerstvu,  formalne metode su posebna vrsta matematički zasnovanih tehnika za specifikaciju, razvoj i verifikaciju softvera i hardvera sistema.[1] Upotreba formalnih metoda za softverski i hardverski dizajn je motivisana očekivanjem da, kao i u drugim inženjerskim disciplinama, obavljanje odgovarajućih matematičkih analiza može doprineti pouzdanosti i robusnosti dizajna.[2]

Formalne metode se najbolje opisuju kao primena prilično širokog spektra teorijskih osnova informatike, posebno logike računanja, formaln og jezika, teorije automata, i programske semantike, ali takođe tipove sistema i algebarske strukture podataka za probleme u softverskoj i hardverskoj specifikaciji i verifikaciji.[3]

Taksonomija uredi

Formalni postupci se mogu koristiti na više nivoa:

Nivo 0: Formalna specifikacija može se preduzeti, a zatim program razviti od ovoga neformalno. Ovo je nazvano formalne metode lite. Ovo može da bude opcija najisplativija u mnogim slučajevima.

Nivo 1: Formalni razvoj i formalna verifikacija se mogu koristiti za proizvodnju programa na formalniji način. Na primer, dokazi o osobinama ili prefinjenosti iz specifikacije na program može se preduzeti. Ovo može biti najprikladnije u sistemima visokog integriteta koji uključuju bezbednost ili sigurnost. 

Nivo 2: Teorema provere može da se koristi da preduzme u potpunosti formalne dokaze mašinski proverene. Ovo može biti veoma skupo i samo praktično isplativo ako je cena grešaka izuzetno visoka (na primer, u kritičnim delovima mikroprocesora dizajna).

Dodatne informacije o tome su ispod proširene.

Kao i kod semantike programskih jezika, stilovi formalnih metoda mogu se grubo klasifikovati na sledeći način:

  • Denotaciona semantika, u kojoj se smisao sistema izražava u matematičkoj teoriji domena. Zagovornici takvih metoda se oslanjaju na dobro razumnu prirodu domena da daju smisao sistema; kritičari ističu svaki sistem koji ne može da se intuitivno ili prirodno pregleda u funkciji.
  • Operativna semantika, u kojoj je smisao sistema izražen kao niz akcija u (verovatno) jednostavnijem  izračunavanju modela. Zagovornici takvih metoda ukazuju na jednostavnost svojih modela kao sredstvo za izražajne jasnoće; kritičari odgovaraju da je problem semantike upravo odložen (koji definiše semantiku od jednostavnijih modela?).
  • Aksiom semantika, u kojoj se smisao sistema izražava u smislu preduslova i postuslova koji su tačni pre i posle obavljanja sistemskog zadatka, respektivno. Zagovornici paze na vezu klasične logike; Kritičari paze da nikada takva semantika zaista ne opisuje šta sistem radi (samo ono što je istinito pre i nakon). 

Lagane formalne metode uredi

Neki stručnjaci veruju da je zajednica formalnih metoda zanemarila punu formalizaciju specifikacije ili dizajna.[4][5] Oni tvrde da ekspresija jezika koji su uključeni, kao i složenost sistema koji se modelira, daje punu formalizaciju teških i skupih zadataka. Kao alternativa, predložene su različite lagane formalne metode, koje naglašavaju delimičnu specifikaciju i fokusiranu aplikaciju. Primeri ovog lakog pristupa formalnih metoda obuhvataju splav objekata modeliranja zapisa,[6] Denijevu sintezu nekih aspekata Z oznaka sa slučaj korišćenja voznog razvoja,[7]i CSK VDM alata.[8]

Upotreba uredi

Formalne metode mogu se primeniti na različitim tačkama u razvojnom procesu.

Specifikacija uredi

Formalne metode se mogu koristiti da daju opis sistemima da se razvijaju, na bilo kojem nivou željenog detalja. Ovaj formalni opis može da se koristi za usmeravanje daljeg razvoja aktivnosti (vidi sledeće odeljke); Pored toga, može da se koristi da proveri da li su zahtevi za razvijen  sistem potpuno i tačno naznačeni.

Potreba za formalnom specifikacijom sistema je istaknuta godinama. U izveštaju ALGOL 58 ,[9] Džon Bakus predstavio je  formalni zapis za opisivanje sintakse programskog jezika (kasnije nazvana Bakus normalna forma kasnije preimenovana Bakus–Naurova forma (BNF)[10]). Bakus je takođe napisao da formalni opis značenja sintaksi važećih Algol programa nije završena na vreme za uključivanje u izveštaj. "Stoga formalni tretman semantike pravnih programa biće uključen u narednom papiru." To se nije pojavilo.

Razvoj uredi

Kada je formalna specifikacija nastala, specifikacija je mogla da se koristi kao vodič dok je beton sistem  razvijen tokom procesa projektovanja (npr, shvatio obično u softveru, ali i potencijalno u hardveru). Na primer:

  • Ako je formalna specifikacija u operativnoj semantici, posmatrano ponašanje konkretnog sistema može se uporediti sa ponašanjem specifikacije (koja je i sama trebo da bude izvršena). Pored toga, operativne komande ove specifikacije mogu biti podložne direktnom prevodu na izvršni kod.
  • Ako je formalna specifikacija  u jednoj aksiomatskoj semantici, preduslovi i posleuslovi u specifikaciji mogu postati tvrdnje u izvršnom kodu.

Verifikacija uredi

Kada je formalna specifikacija razvijena, specifikacija je mogla da se koristiti kao osnova za dokazivanje svojstva specifikacije (i nadamo se zaključivanjem razvijenog sistema).

Ljudski usmeren dokaz uredi

Ponekad motivacija za dokazivanje ispravnosti sistema nije očigledna potreba za re-osiguranje ispravnosti sistema, ali je želja da se bolje razumeju sistemi. Shodno tome, neki dokazi o korektnosti su proizvedeni u stilu matematičkih dokaza: u rukopisu (ili slagala) koristeći prirodni jezik, koristeći nivo neformalnog zajedničkog takvog dokaza. "Dobar" dokaz je onaj koji je čitljiv i razumljiv od strane drugih ljudskih čitalaca.

Kritičari ovakvog pristupa ističu da je dvosmislenost svojstvena prirodnom jeziku i da dozvoljava greške da se nađu neprimećeno u takvim dokazima; Često, suptilne greške mogu biti prisutne u detaljima na niskom nivou obično previde takvih dokaza. Osim toga, rad uključen u izradu tako dobrog dokaza zahteva visok nivo matematičke sofisticiranosti i stručnosti.

Automatski dokaz uredi

Nasuprot tome, postoji sve veće interesovanje u proizvodnji dokaza o ispravnosti takvih sistema i automatski način. Automatizovane tehnike spadaju u tri kategorije:

  • Automatsko dokazivanje teorema, u kojem sistem pokušava da proizvede formalni dokaz od nule, s obzirom na opis sistema, skup logičkih aksioma, i skup pravila zaključivanja.
  • Provera modela, u kojoj sistem proverava određene osobine pomoću iscrpnih potraga za svim mogućim zemaljama da sistem uđe u njegovo izvršenje. 
  • Apstraktna interpretacija, u kojoj sistem proverava preterano približavanje nekog ponašanja imovine programa, koristeći fikpoint računanje preko (eventualno) kompletne rešetke ga zastupa.

Neke automatizovane teorema provere zahtevaju smernice o tome koje osobine su "zanimljive" da nastave, dok drugi rade bez ljudske intervencije. Model provere može  brzo da vas zakoči u proveri milion nezanimljivih država, ako ne daje dovoljno apstraktni model.

Zagovornici takvih sistema tvrde da rezultati imaju veću matematičku sigurnost od ljudskih proizvedenih dokaza, jer svi zamorni detalji su algoritmički provereni. Potrebe treninga  da koristi takve sisteme je takođe manje nego što je potrebno da proizvede dobre matematičke dokaze rukom, izradu tehnike dostupne različitim praktičarima.

Kritičari imaju na umu da neki od tih sistema su kao proročanstava: prave izricanje istine, ali ne daju objašnjenje te istine. Tu je i problem "provere verifikatora"; ako program koji pomaže u verifikaciji sam po sebi nije dokazan, može biti razlog da se sumnja u ispravnost proizvedenih rezultata. Neki alati modernog modela provere proizvode "dokaz dnevnik" detaljno svaki korak u njihovom dokazu, tako da je moguće da se izvrši, s obzirom na odgovarajući alat, nezavisna verifikacija.

Glavna karakteristika apstraktnog pristupa tumačenju je da pruža dobru analizu, odnosno nema laži, se vratila. Štaviše, to je efikasno prilagodljivo, podešavanje apstraktnog domena predstavlja imovinu koja se analizira, a primenom proširenja operatera[11] da se brzo približava.

Aplikacije uredi

Formalne metode se primenjuju u različitim oblastima hardvera i softvera, uključujući rutere, eksterne prekidače, usmeravanje protokola i bezbednosti aplikacija. Postoji nekoliko primera u kojima su korišćeni za proveru funkcionalnosti hardvera i softvera koji se koristi u DCs. IBM koristi ACL2, a teoremu provere, u procesu izrade AMD x86 procesora. Intel koristi takve metode da proveri svoj hardver i firmvare (stalni softver programiran u memorija samo za čitanje). Dansk Datamatik Center  koristi formalne metode u 1980 da razvije prevodilac sistem za Ada programski jezik koji je otišao da postane dugovečni komercijalni proizvod.[12][13]

Postoji nekoliko drugih projekata NASE u kojima se primenjuju formalne metode, kao što je   Sledeća generacija vazdušnog transportnog sistema, Unmanned Aircraft System integration in National Airspace System,[14] i Airborne Coordinated Conflict Resolution and Detection (ACCoRD).[15] B-Method sa AtelierB,[16] se koristi za razvoj bezbednosti automatizama za razne metroe instalirane širom sveta od strane  Alstom i Siemens, kao i za zajedničke kriterijume sertifikace i razvoj modela sistema od ATMEL i  STMicroelectronics.

Formalna verifikacija je često korišćena u hardveru većine poznatih hardvera, kao što su IBM, Intel, i AMD. Postoje mnoge oblasti hardvera, gde  Intel koristii FMS da proveri funkcionisanje proizvoda, kao što su parametrizovana verifikacija keša koherentnost protokola,[17] Intel Core i7 procesor validacija izvršenja motora [18] (koristeći dokazivanje teorema, BDD’s, i simboličku evaluaciju), optimizacija za Intel IA-64 arhitekturu koristeći HOL svetlo teoremu provere,[19] i verifikacija visokih performansi dual-port  eksterni kontroler sa podrškom za PS ekspres protokol i Intel naprednu tehnologiju za upravljanje pomoću ritma.[20] Slično tome, IBM je koristio formalne metode u verifikaciji moći kapije,[21] registri,[22] i funkcionalna verifikacija IBM Power7 mikroprocesora.[23]

Formalne metode i oznake uredi

Postoji niz formalnih metoda i oznaka na raspolaganju.

Specifikacija jezika
Modeli provere
  • SPIN
  • Pat je moćan besplatan model provere, simulator i prefinjen model provere za istovremene sisteme i SPRS lokale (npr zajedničke varijable, nizovi, pravičnost).
  • MALPAS Software Static Analysis Toolset je industrijski snažni model provere koji se koristi za formalni  dokaz o sigurnosti kritičnih sistema
  • UPPAAL

Vidi još uredi

Reference uredi

  1. ^ R. W. Butler (6. 8. 2001). „What is Formal Methods?”. Pristupljeno 16. 11. 2006. 
  2. ^ C. Michael Holloway. „Why Engineers Should Consider Formal Methods” (PDF). 16th Digital Avionics Systems Conference (27–30 October 1997). Arhivirano iz originala 06. 06. 2012. g. Pristupljeno 16. 11. 2006. 
  3. ^ Monin, str. 3–4
  4. ^ Daniel Jackson and Jeannette Wing, "Lightweight Formal Methods", IEEE Computer, April 1996
  5. ^ Vinu George and Rayford Vaughn, archive "Application of Lightweight Formal Methods in Requirement Engineering", Crosstalk: The Journal of Defense Software Engineering, January 2003
  6. ^ Daniel Jackson, "Alloy: A Lightweight Object Modelling Notation", ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 11, Issue 2 (April ). (2002). str. 256—290
  7. ^ Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality, Addison-Wesley Professional Publishing. 2005. ISBN 0-321-31643-6
  8. ^ 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
  9. ^ 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. 
  10. ^ Knuth, Donald E. (1964), Backus Normal Form vs Backus Naur Form.
  11. ^ A.Cortesi and M.Zanioli, Widening and Narrowing Operators for Abstract Interpretation Arhivirano na sajtu Wayback Machine (23. septembar 2015).
  12. ^ Bjørner et al. 2011, str. 350–359
  13. ^ 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. str. 42—61. 
  14. ^ Gheorghe, A. V., & Ancel, E. (2008, November).
  15. ^ Airborne Coordinated Conflict Resolution and Detection, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/ Arhivirano na sajtu Wayback Machine (5. mart 2016)
  16. ^ website : http://www.atelierb.eu/en/ Arhivirano na sajtu Wayback Machine (13. januar 2016)
  17. ^ C. T. Chou, P. K. Mannava, S. Park, “A simple method for parameterized verification of cache coherence protocols,” Formal Methods in Computer-Aided Design. str. 382-398, 2004.
  18. ^ Formal Verification in Intel® Core™ i7 Processor Execution Engine Validation, http://cps-vo.org/node/1371 Arhivirano na sajtu Wayback Machine (3. maj 2015), accessed at Sep. 13, 2013.
  19. ^ J. Grundy, “Verified optimizations for the Intel IA-64 architecture,” In Theorem Proving in Higher Order Logics, Springer Berlin Heidelberg. (2004). str. 215—232.
  20. ^ E. Seligman, I. Yarom, “Best known methods for using Cadence Conformal LEC,” at Intel.
  21. ^ C. Eisner, A. Nahir, K. Yorav, “Functional verification of power gated designs by compositional reasoning,” Computer Aided Verification Springer Berlin Heidelberg. str. 433-445.
  22. ^ P. C. Attie, H. Chockler, “Automatic verification of fault-tolerant register emulations,” Electronic Notes in Theoretical Computer Science, vol. 149, no. 1. str. 49-60.
  23. ^ 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, vol. 55, no 3.

Literatura uredi

  • Ovaj članak je zasnovan na materijalu preuzetom iz Free On-line Dictionary of Computing do 1. novembra 2008. godine i ugrađen je pod "relicenciranjem" pod GFDL, verzija 1.3 ili novije.
  • 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”. Ur.: Impagliazzo, John; Lundin, Per; Wangler, Benkt. History of Nordic Computing 3: IFIP Advances in Information and Communication Technology. Springer. str. 350—359. 

Spoljašnje veze  uredi

Preuzeto iz „https://sr.wikipedia.org/w/index.php?title=Формалне_методе&oldid=27673158”