Metodat formale

Në shkencën kompjuterike, metodat formale janë teknika matematikisht rigoroze për specifikimin, zhvillimin, analizën dhe verifikimin e sistemeve të softuerit dhe harduerit. Aplikimi i metodave formale në projektimin e softuerit dhe harduerit nxiset nga presioni që, ashtu si në fusha të tjera inxhinierike, realizimi i analizave të nevojshme matematikore mund të ndihmojë në rritjen e qëndrueshmërisë dhe besueshmërisë së një projekti.

Teknikat formale përdorin një shumëllojshmëri themelesh teorike të shkencës kompjuterike, duke përfshirë llogaritjet logjike, gjuhët formale, teorinë e automatëve, teorinë e kontrollit, semantikën e programit, sistemet e tipit dhe teorinë e tipit.

Përdorimet

Teknikat formale mund të përdoren në faza të ndryshme gjatë procesit të zhvillimit.

Specifikimi

Metodat formale mund të shfrytëzohen për të ofruar një përshkrim të saktë të sistemit që do të krijohet, në çdo nivel detajimi që është i kërkuar. Metoda të tjera formale mund të bazohen në këtë specifikim për të krijuar një program ose për të kontrolluar saktësinë e një sistemi.

Ndryshe, përshkrimi mund të jetë faza e vetme ku aplikohet përdorimi i metodave formale.Duke krijuar një përshkrim, pasiguri në kërkesat joformale mund të identifikohen dhe të zgjidhen. Gjithashtu, inxhinierët mund të shfrytëzojnë një përshkrim zyrtar si udhëzues për të orientuar proceset e tyre të zhvillimit.

Kerkesa 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, pas kohes u quajt Backus forma normale në vijim u emërua si formë Backus–Naur (BNF). Backus gjithashtu theksoi se një përshkrim formal i kuptimit të programeve ALGOL që ishin sintaksikisht të vlefshme 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 botua kurrë.

Sinteza

Sinteza e programit është procesi i krijimit automatik të një programi që përputhet me një përshkrim. Qasjet e sintezës deduktive mbështeten në një përshkrim të plotë dhe formalisht të saktë të programit, ndërsa qasjet induktive nxjerrin përshkrime nga shembuj. Sintetizuesit kryejnë një kërkim në hapësirën e mundshme të programeve për të gjetur një program që përmbush specifikimet. Për shkak të shkallës së gjerë të kësaj hapësire kërkimi, zhvillimi i algoritmeve efikas për kërkim mbetet një nga sfidat kryesore në sintezën e softuerit.

Verifikimi

Vërtetimi formal është shfrytëzimi i paisjeve softuerike për të konfirmuar karakteristikat e një specifikimi formal, ose për të vërtetuar se një model formal i zbatimit të një sistemi plotëson kerkesat e tij.

Pasi të jetë zgjeruar një specifikim formal, specifikimi mund të shfrytëzohet si themel për të vërtetuar karakteristikat e specifikimit, dhe me konkluzion, karakteristikat e zbatimit të sistemit.

Verifikimi i hyrjes

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

Prova e drejtuar nga njeriu

Ndonjëherë, motivimi për të verifikuar korrektësinë e një sistemi nuk është e domosdoshme për të garantuar besueshmërinë dhe saktësinë e sistemit, por gjithashtu për të pasur një kuptim më të thellë të tij.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 kuptueshme dhe e lehtë për t'u lexuar nga njerëzit e tjerë.

Ata që kritikojnë qasje të tilla theksojnë se paqartësia në gjuhën natyrore lejon që gabimet të mos identifikohen në prova të tilla; shpesh, gabime të imëta mund të jenë të pranishme në detajet e nivelit të ulët, të cilat zakonisht injorohen nga prova të tilla. Për më tepër, puna e angazhuar në krijimin e një prove kaq të saktë kërkon një nivel të lartë të sofistikimit dhe njohurive të avancuara matematikore.

Dëshmi e automatizuar

Përkundrazi, ka një interes në rritje për të krijuar prova të saktësisë së sistemeve të tilla duke përdorur mjete të automatizuara. Teknikat automatike ndahen në tre grupe 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 për të përcaktuar cilat veçori janë mjaft 'interesante' për t'u ndjekur, ndërsa të tjerë veprojnë pa ndërhyrjen e njeriut. Defektet e modeleve mund të shfaqen shpejt gjatë kontrollimit të miliona gjendjeve të padobishme nëse nuk ofrohet një model mjaft abstrakt.

Përkrahësit e sistemeve të tilla argumentojnë se rezultatet ofrojnë një sigurim më të madh matematikor sesa provat e krijuara nga njeriu, pasi të gjitha detajet e mundimshme 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ë sakta matematikore manualisht, duke i bërë këto teknika më të disponueshme për një gamë më të gjerë praktikuesish.

Kritikët theksojnë se disa nga këto sisteme janë si orakuj: ato shpallin një të vërtetë, por nuk ofrojnë asnjë shpjegim për këtë të vërtetë. Ekziston edhe problemi i " verifikimit të verifikuesit "; nëse programi që ndihmon në verifikim është vetë i paprovuar, mund të lindin dyshime për qëndrueshmërinë e rezultateve të prodhuara. Disa mjete moderne për kontrollin e modeleve krijojnë një 'regjistër provash' që detajon çdo hap të provës së tyre, duke mundësuar, nëse disponohen mjetet e duhura, verifikimin e pavarur.

Karakteristika kryesore e qasjes së interpretimit abstrakt është se ajo ofron një analizë të saktë, duke shmangur rezultatet negative të rreme. Për më tepër, ajo është e shkallëzueshme në mënyrë efikase, duke përshtatur domenin abstrakt që përfaqëson vetinë që do të analizohet, dhe duke aplikuar operatorë zgjerues për të arritur konvergjencë të shpejtë.

Teknikat

Metodat formale përfshijnë një serë teknikash të ndryshme.

Specifikimet e gjuhëve

Dizajni i një sistemi kompjuterik mund të shpjegohet duke përdorur një gjuhë specifikimi, ajo që është një gjuhë zyrtare që përmban një sistem provash. Duke shfrytëzuar këtë sistem provash, mjetet zyrtare të verifikimit mund të demonstrohet për specifikimin dhe të specifikojnë se një sistem i përmbahet specifikimit.

Diagramet e vendimeve binare

Vendimi i një diagrami binar ë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 P shpreh që një ekzekutim i caktuar i një programi është në përputhje me specifikimin, atëherë përcaktimi që ¬P është i pakënaqshëm është ekuivalent me përcaktimin që të gjitha ekzekutimet janë në përputhje me specifikimet. Zgjidhësit SAT përdoren shpesh në kontrollin e modeleve të kufizuara, por mund të përdoren gjithashtu edhe për kontrollin e modeleve të pakufizuara.

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. Përmenden disa shembuj në të cilët ato janë përdorur për të konfirmuar funksionalitetin e harduerit dhe softuerit të përdorur në qendrat e të dhënave. IBM përdori ACL2, një dëshmi teoreme, në procesin e zhvillimit të procesorit AMD x86.  Intel përdor teknika 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, 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. Keto metodat 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ë Metoda-B, 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ë shyqrtohen zyrtarisht.

Për softuerin dhe sistemet e njëkohshme, rrjetat Petri, algjebra e proceseve 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) mundësojnë specifikimet e softuerit të ekzekutueshëm dhe mund të përdoren për të ndërtuar dhe verifikuar 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.

Metodat gjysmë formale

Metodat gjysmë formale janë formalizma dhe gjuhë që nuk konsiderohen plotësisht "formale".Ai e shtyn detyrën e plotësimit të semantikës në një fazë të mëvonshme, e cila më pas bëhet ose me interpretim njerëzor ose me interpretim përmes softuerëve si gjeneratorë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 Alloy, 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 në dispozicion.

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

Kontrollues të modeleve

• 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

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

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

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

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 Arkivuar 2012-06-08 tek Wayback Machine projekti (EU FP7) në Archive.org