Përdoruesi:Yllka Dedinca/Metodat formale

Në shkencën kompjuterike, metodat formale janë teknika matematikisht rigoroze për specifikimin, zhvillimin, analizën dhe verifikimin e sistemeve softuerike dhe harduerike.Përdorimi i metodave formale në dizajnimin e softuerit dhe harduerit bazohet në idenë që, ashtu si në disiplinat e tjera inxhinierike, kryerja e analizave të sakta matematikore mund të rrisë besueshmërinë dhe qëndrueshmërinë e dizajnit.

Metodat formale përdorin një sërë bazash teorike të shkencës kompjuterike, duke përfshirë llogaritjet logjike, gjuhët formale, teorinë e automatëve, teorinë e kontrollit, semantikën e programeve, sistemet e tipit dhe teorinë e tipit.

Përdorimet

Metodat formale mund të aplikohen në pika të ndryshme gjatë procesit të zhvillimit.

Specifikimi

Metodat formale mund të përdoren për të paraqitur sistemet që do të krijohen në një mënyrë të strukturuar dhe të qartë, në çdo shkallë detajimi që është e nevojshme. Ky paraqitje mund të shërbejë si themel për teknika të tjera formale që kanë për qëllim krijimin e një programi nga ky specifikim ose për të verifikuar saktësinë e funksionimit të sistemit.

Përndryshe, specifikimi mund të jetë faza e vetme ku aplikohen metodat formale. Duke hartuar një specifikim, pasiguri në kërkesat joformale mund të identifikohen dhe të adresohen. Për më tepër, inxhinierët mund të përdorin një specifikim zyrtar si udhëzues për të orientuar proceset e tyre të zhvillimit.

Nevoja për sisteme të specifikimeve formale është vërejtur prej vitesh. Në raportin e ALGOL 58,John Backus prezantoi një shënim zyrtar për përshkrimin e sintaksës së gjuhës programuese, më vonë u quajt Backus forma normale më pas u riemërua në formë Backus–Naur (BNF). Backus gjithashtu shkroi se një përshkrim formal i kuptimit të programeve ALGOL të vlefshme sintaksisht nuk ishte përfunduar në kohë për t'u përfshirë në raport, duke deklaruar se "do të përfshihet në një dokument të mëvonshëm".Sidoqoftë, asnjë dokument që përshkruan semantikën formale nuk u publikua kurrë.

Sinteza

Stampa:Computer scienceSinteza e programit është procesi i krijimit automatik të një programi që i përgjigjet një specifikimi. Qasjet e sintezës deduktive mbështeten në një specifikim të plotë dhe formalisht të saktë të programit, ndërsa qasjet induktive nxjerrin specifikimet nga shembujt. Sintetizuesit realizojnë një kërkim në hapësirën e mundshme të programeve për të gjetur një program që është në përputhje me specifikimet. Për shkak të përmasave të mëdha të kësaj hapësire kërkimi, zhvillimi i algoritmeve efikasë të kërkimit është një nga sfidat kryesore në sintezën e programit.

Verifikimi

Verifikimi formal është përdorimi i mjeteve softuerike për të vërtetuar vetitë e një specifikimi formal, ose për të vërtetuar se një model formal i një zbatimi të sistemit plotëson specifikimet e tij.

Pasi të jetë zhvilluar një specifikim formal, specifikimi mund të përdoret si bazë për të vërtetuar vetitë e specifikimit, dhe me konkluzion, vetitë e zbatimit të sistemit.

Verifikimi i hyrjes

Verifikimi i hyrjes është përdorimi i një mjeti zyrtar verifikimi me besueshmëri të lartë. Një mjet i tillë mund të zëvendësojë metodat tradicionale të verifikimit (mjeti mund të jetë gjithashtu i certifikuar).

Prova e drejtuar nga njeriu

Ndonjëherë, motivimi për të vërtetuar korrektësinë e një sistemi nuk është nevoja e dukshme për të siguruar sigurinë e korrektësisë së sistemit, por dëshira për të kuptuar më mirë sistemin. Rrjedhimisht, disa prova të korrektësisë prodhohen në stilin e provës matematikore : të shkruara me dorë (ose të shtypura) duke përdorur gjuhën natyrore, duke përdorur një nivel informaliteti të përbashkët për prova të tilla. Një provë "e mirë" është ajo që është e lexueshme dhe e kuptueshme nga lexuesit e tjerë njerëzorë.

Kritikët e qasjeve të tilla theksojnë se paqartësia e natyrshme në gjuhën natyrore lejon që gabimet të mos zbulohen në prova të tilla; shpesh, gabimet delikate mund të jenë të pranishme në detajet e nivelit të ulët që zakonisht anashkalohen nga prova të tilla. Për më tepër, puna e përfshirë në prodhimin e një prove kaq të mirë kërkon një nivel të lartë të sofistikimit dhe ekspertizës matematikore.

Dëshmi e automatizuar

Në të kundërt, ka një interes në rritje për të krijuar prova të korrektësisë së sistemeve të tilla me mjete automatike. Teknikat automatike ndahen në tri kategori kryesore:

• Prova e automatizuar e teoremës, në të cilën një sistem përpiqet të prodhojë një provë formale nga e para, duke pasur parasysh një përshkrim të sistemit, një grup aksiomash logjike dhe një sërë rregullash konkluzionesh .
• Kontrollimi i modelit, në të cilin një sistem verifikon veti të caktuara me anë të një kërkimi shterues të të gjitha gjendjeve të mundshme që një sistem mund të hyjë gjatë ekzekutimit të tij.
• Interpretimi abstrakt, në të cilin një sistem verifikon një mbi-përafrim të një vetie të sjelljes së programit, duke përdorur një llogaritje të pikës fikse mbi një rrjetë (ndoshta të plotë) që e përfaqëson atë.

Disa prova të automatizuara të teoremave kërkojnë udhëzime se cilat prona janë mjaft "interesante" për t'u ndjekur, ndërsa të tjerët punojnë pa ndërhyrjen njerëzore. Damët e modeleve mund të zhyten shpejt në kontrollimin e miliona gjendjeve jo interesante nëse nuk i jepet një model mjaft abstrakt.

Përkrahësit e sistemeve të tilla argumentojnë se rezultatet kanë një siguri më të madhe matematikore sesa provat e krijuara nga njeriu, pasi të gjitha detajet e lodhshme janë verifikuar në mënyrë algoritmike. Trajnimi i nevojshëm për përdorimin e sistemeve të tilla është gjithashtu më i vogël se ai që kërkohet për të krijuar prova të mira matematikore me dorë, duke i bërë teknikat të arritshme për një gamë më të gjerë praktikuesish.

Kritikët vënë në dukje se disa nga ato sisteme janë si orakuj : ata bëjnë një shpallje të së vërtetës, por nuk japin asnjë shpjegim për këtë të vërtetë. Ekziston edhe problemi i " verifikimit të verifikuesit "; nëse programi që ndihmon në verifikimin është vetë i paprovuar, mund të ketë arsye për të dyshuar në qëndrueshmërinë e rezultateve të prodhuara. Disa mjete moderne të kontrollit të modeleve prodhojnë një "regjistër provash" që detajon çdo hap në provën e tyre, duke bërë të mundur kryerjen, duke pasur parasysh mjetet e përshtatshme, të verifikimit të pavarur.

Karakteristika kryesore e qasjes së interpretimit abstrakt është se ofron një analizë të saktë, pra nuk gjenerohen falsifikime negative. Për më tepër, ajo është e shkallëzueshme në mënyrë efikase, duke akorduar domenin abstrakt që përfaqëson vetinë që do të analizohet dhe duke aplikuar operatorë të zgjeruarpër të marrë konvergjencë të shpejtë.

Teknikat

Metodat formale përfshijnë një sërë teknikash të ndryshme.

Specifikimet e gjuhëve

Dizajni i një sistemi kompjuterik mund të shprehet përmes një gjuhe specifikimi, e cila është një gjuhë zyrtare që përfshin një sistem provash. Duke përdorur këtë sistem provash, mjetet zyrtare të verifikimit mund të arsyetojnë për specifikimin dhe të përcaktojnë nëse një sistem i përmbush kërkesat e specifikimit.

Diagramet e vendimeve binare

Një diagram binar vendimi është një strukturë e të dhënave që përfaqëson një funksion Boolean. Nëse një formulë Boolean ${\mathcal {P}}$ shpreh se një ekzekutim i një programi përputhet me specifikimin, një diagram vendimi binar mund të përdoret për të përcaktuar nëse ${\mathcal {P}}$ është një tautologji; dmth vlerëson gjithmonë të VËRTETË. Nëse është kështu, atëherë programi përputhet gjithmonë me specifikimet.

Zgjidhësit SAT

Një zgjidhës SAT është një program që mund të zgjidhë problemin e kënaqshmërisë Boolean, problemin e gjetjes së një caktimi të variablave që e bën një formulë të dhënë propozimi të vlerësohet si e vërtetë. Nëse një formulë Boolean ${\mathcal {P}}$ shpreh se një ekzekutim specifik i një programi përputhet me specifikimin, duke përcaktuar më pas atë $\neg {\mathcal {P}}$ është e pakënaqshme është ekuivalente me përcaktimin se të gjitha ekzekutimet janë në përputhje me specifikimet. Zgjidhësit SAT përdoren shpesh në kontrollimin e modelit të kufizuar, por mund të përdoren gjithashtu në kontrollin e modelit të pakufishëm.

Aplikacionet

Metodat formale aplikohen në fusha të ndryshme të harduerit dhe softuerit, duke përfshirë ruterat, ndërprerësit Ethernet, protokollet e rrugëtimit, aplikacionet e sigurisë dhe mikrokernelet e sistemit operativ si seL4 . Ka disa shembuj në të cilët ato janë përdorur për të verifikuar funksionalitetin e harduerit dhe softuerit të përdorur në qendrat e të dhënave . IBM përdori ACL2, një provë teoreme, në procesin e zhvillimit të procesorit AMD x86.  Intel përdor metoda të tilla për të verifikuar harduerin dhe firmuerin e saj (softuer i përhershëm i programuar në një memorie vetëm për lexim )  . Qendra Dansk Datamatik përdori metoda formale në vitet 1980 për të zhvilluar një sistem përpilues për gjuhën e programimit Ada që vazhdoi të bëhej një produkt tregtar jetëgjatë.

Ka disa projekte të tjera të NASA-s në të cilat aplikohen metoda formale, si Sistemi i Transportit Ajror të Gjeneratës së ardhshme </link>, Integrimi i Sistemit të Avionëve pa pilot në Sistemin Kombëtar të Hapësirës Ajrore, dhe Zgjidhja dhe Zbulimi i Koordinuar i Konflikteve në Ajr (ACCoRD). B-Method me Atelier B, përdoret për të zhvilluar automatizma sigurie për metrotë e ndryshme të instaluara në të gjithë botën nga Alstom dhe Siemens, si dhe për certifikimin e kritereve të përbashkëta dhe zhvillimin e modeleve të sistemit nga ATMEL dhe STMicroelectronics .

Verifikimi zyrtar është përdorur shpesh në harduer nga shumica e shitësve të njohur të pajisjeve, si IBM,Intel dhe AMD. Ka shumë fusha të harduerit, ku Intel ka përdorur metoda formale për të verifikuar funksionimin e produkteve, të tilla si verifikimi i parametrizuar i protokollit koherent në cache,vërtetimi i motorit të ekzekutimit të procesorit Intel Core i7 (duke përdorur vërtetimin e teoremës,BDD, dhe vlerësimi simbolik), optimizimi për arkitekturën Intel IA-64 duke përdorur proverin e teoremës së dritës HOL, dhe verifikimin e Kontrollues Ethernet gigabit me dy porta me performancë të lartë me mbështetje për protokollin PCI express dhe teknologjinë e menaxhimit të avancimit Intel duke përdorur Cadence. Në mënyrë të ngjashme, IBM ka përdorur metoda formale në verifikimin e portave të energjisë, regjistrat, dhe verifikimin funksional të mikroprocesorit IBM Power7.

Në zhvillimin e softuerit

Në zhvillimin e softuerit, metodat formale janë qasje matematikore për zgjidhjen e problemeve të softuerit (dhe harduerit) në kërkesat, specifikimet dhe nivelet e projektimit. Metodat formale kanë më shumë gjasa të aplikohen në softuerët dhe sistemet kritike për sigurinë ose sigurinë, të tilla si softueri avionik . Standardet e sigurimit të sigurisë së softuerit, të tilla si DO-178C lejojnë përdorimin e metodave formale përmes plotësimit, dhe Kriteret e Përbashkëta urdhërojnë metodat formale në nivelet më të larta të kategorizimit.

Për softuerin sekuencial, shembuj të metodave formale përfshijnë B-Method, gjuhët e specifikimeve të përdorura në vërtetimin e automatizuar të teoremës, RAISE dhe shënimin Z.

Në programimin funksional, testimi i bazuar në veti ka lejuar specifikimin dhe testimin matematikor (nëse jo testim shterues) të sjelljes së pritshme të funksioneve individuale.

Gjuha e kufizimit të objektit (dhe specializimet si gjuha e modelimit Java ) ka lejuar që sistemet e orientuara nga objekti të specifikohen zyrtarisht, nëse jo domosdoshmërisht të verifikohen zyrtarisht.

Për softuerët dhe sistemet e njëkohshme, rrjetat Petri, algjebra e procesit dhe makinat e gjendjes së fundme (të cilat bazohen në teorinë e automatave ; shih gjithashtu makinën virtuale të gjendjes së fundme ose makinën e gjendjes së fundme të drejtuar nga ngjarjet ) lejojnë specifikimet e softuerit të ekzekutueshëm dhe mund të përdoren për të ndërtuar dhe vërtetuar sjelljen e aplikimit.

Një qasje tjetër ndaj metodave formale në zhvillimin e softuerit është të shkruani një specifikim në një formë logjike - zakonisht një variacion i logjikës së rendit të parë - dhe më pas të ekzekutoni drejtpërdrejt logjikën sikur të ishte një program. Gjuha OWL, e bazuar në logjikën e përshkrimit, është një shembull. Ka gjithashtu punë për hartimin e një versioni të anglishtes (ose një gjuhë tjetër natyrore) automatikisht në dhe nga logjika, si dhe ekzekutimin e logjikës drejtpërdrejt. Shembuj janë Anglishtja e kontrolluar e tentativës dhe logjika e biznesit në internet, të cilat nuk kërkojnë të kontrollojnë fjalorin ose sintaksën. Një tipar i sistemeve që mbështesin hartëzimin dydrejtues të logjikës angleze dhe ekzekutimin e drejtpërdrejtë të logjikës është se ato mund të bëhen për të shpjeguar rezultatet e tyre, në anglisht, në nivel biznesi ose shkencor. </link>

Metodat gjysmë formale

Metodat gjysmë formale janë formalizma dhe gjuhë që nuk konsiderohen plotësisht "formale". Ato e shtyjnë detyrën e përfundimit të semantikës në një fazë të mëvonshme, e cila më pas realizohet ose me interpretim njerëzor, ose me interpretim përmes softuerëve, sigjeneratorët e kodeve ose rasteve testuese.

Disa praktikues besojnë se komuniteti i metodave formale e ka mbitheksuar formalizimin e plotë të një specifikimi ose dizajni. Ata pretendojnë se ekspresiviteti i gjuhëve të përfshira, si dhe kompleksiteti i sistemeve që modelohen, e bëjnë formalizimin e plotë një detyrë të vështirë dhe të shtrenjtë. Si alternativë, janë propozuar metoda të ndryshme formale të lehta, të cilat theksojnë specifikimin e pjesshëm dhe aplikimin e fokusuar. Shembuj të kësaj qasjeje të lehtë ndaj metodave formale përfshijnë shënimin e modelimit të objektit Aloy, sintezën e Denney-t të disa aspekteve të shënimit Z me zhvillimin e drejtuar nga rasti i përdorimit, dhe CSK VDM Tools.

Metodat dhe shënimet formale

Ekzistojnë një sërë metodash dhe shënimesh formale të disponueshme.

Specifikimet e gjuhëve

• Makinat e gjendjes abstrakte (ASM)
• Një Logjikë Llogaritëse për Lispën e Përbashkët Aplikative (ACL2)
• Aktor model
• aliazh
• Gjuha e specifikimit ANSI/ISO C (ACSL)
• Gjuha e specifikimit të sistemit autonom (ASSL)
• B-Metoda
• CADP
• Gjuha e zakonshme e specifikimeve algjebrike (CASL)
• Esterel
• Gjuha e modelimit Java (JML)
• Asistent i softuerit të bazuar në njohuri (KBSA)
• Shkëlqim
• mCRL2
• Zhvilluesi i përsosur
• rrjeta Petri
• Programimi predikativ
• Llogaritjet e procesit
  • CSP
  • LOTOS
  • π-llogaritje
• NGRITJE
• Rebeca Modeling Language
• SPARK Ada
• Specifikimet dhe gjuha e përshkrimit
• TLA+
• USL
• VDM
  • VDM-SL
  • VDM++
• Shënimi Z

Damë model

• ESBMC
• Kompleti i veglave të analizës statike të softuerit MALPAS – një kontrollues modeli me forcë industriale që përdoret për vërtetimin zyrtar të sistemeve kritike për sigurinë
• PAT – një kontrollues modeli, simulator dhe kontrollues i përsosjes falas për sistemet e njëkohshme dhe shtesat CSP (p.sh., variabla të përbashkëta, vargje, drejtësi)
• TRETJE
• UPPAAL

Zgjidhësit dhe konkurset

Shumë probleme në metodat formale janë NP-të vështira, por mund të zgjidhen në rastet që dalin në praktikë. Për shembull, problemi i kënaqshmërisë Boolean është NP-komplet nga teorema Cook–Levin, por zgjidhësit SAT mund të zgjidhin një sërë shembujsh të mëdhenj. Ka "zgjidhës" për një sërë problemesh që lindin në metodat formale dhe ka shumë konkurse periodike për të vlerësuar teknologjinë më të fundit në zgjidhjen e problemeve të tilla.

• Konkursi SAT është një konkurs vjetor që krahason zgjidhësit SAT. Zgjidhësit SAT përdoren në mjetet e metodave formale siç është Alloy .
• CASC është një konkurs vjetor i provave të automatizuara të teoremave .
• SMT-COMP është një konkurs vjetor i zgjidhësve SMT, të cilët aplikohen për verifikimin zyrtar .
• CHC-COMP është një konkurs vjetor i zgjidhësve të klauzolave të kufizuara Horn,të cilat kanë aplikime për verifikimin zyrtar.
• QBFEVAL është një konkurs dyvjeçar i zgjidhësve për formula të vërteta të kuantifikuara Boolean, të cilat kanë aplikime për kontrollimin e modeleve.
• SV-COMP është një konkurs vjetor për mjetet e verifikimit të softuerit.
• SyGuS-COMP është një konkurs vjetor për mjetet e sintezës së programeve.

Organizatat

• Metodat formale në Evropë (FME)
• Metodat formale Wiki
• Metodat formale nga Foldoc

Shihni gjithashtu

• Interpretimi abstrakt
• Vërtetimi i automatizuar i teoremës
• Projektim me kontratë
• Metodat formale njerëzit
• Shkenca formale
• Specifikimi formal
• Verifikimi formal
• Sistemi formal
• Metodizmi
• Metodologjia
• Kontrollimi i modelit
• Metoda shkencore
• Inxhinieri softuerike
• Gjuha e specifikimeve

Lidhje të jashtme

• BCS-FACS
• Metodat formale në Evropë
• Z Grupi i përdoruesve

Material arkivor

• Fjalë kyçe e metodës formale në Kërkimin Akademik të Microsoft nëpërmjet Archive.org
• Dëshmi mbi përdorimet dhe ndikimin e metodave formale në industri të mbështetur nga DEPLOY Archived </link> projekti (BE FP7) në Archive.org

[[Kategoria:Specifikimet e gjuheve]] [[Kategoria:Shkenca kompjuterike teorike]] [[Kategoria:Filozofitë e zhvillimit të softuerit]] [[Kategoria:Metodat formale]] [[Kategoria:Artikuj me lidhje të jashtme të vdekura përfundimisht]] [[Kategoria:Artikuj me lidhje të jashtme të vdekura nga nëntori 2022]] [[Kategoria:Artikuj me lidhje të jashtme të vdekura]] [[Kategoria:Faqe me përkthime të pashqyrtuara]]