Formalus verifikavimas

Straipsnis iš Vikipedijos, laisvosios enciklopedijos.
Jump to navigation Jump to search
 Broom icon.svg  Šį puslapį ar jo dalį reikia sutvarkyti pagal Vikipedijos standartus.
Jei galite, sutvarkykite.
 Crystal Clear action spellcheck.png  Šį straipsnį ar jo skyrių reikėtų peržiūrėti.
Būtina ištaisyti gramatines klaidas, patikrinti rašybą, skyrybą, stilių ir pan.
Ištaisę pastebėtas klaidas, ištrinkite šį pranešimą ir apie tai, jei norite, praneškite Tvarkos projekte.
 NoFonti.svg  Šiam straipsniui ar jo daliai trūksta šaltinių ar nuorodų į juos.
Jūs galite padėti Vikipedijai įrašydami tinkamas išnašas ar nuorodas į šaltinius.

Formalusis verifikavimas - yra veiksmas patvirtinti ar paneigti numatomų algoritmų teisingumą, pabrėžiant sistemą ir atsižvelgiant į tam tikrą formalią ypatybių specifikaciją, naudojant formaliuosius matematikos metodus.

Naudojimas[redaguoti | redaguoti vikitekstą]

Formalusis verifikavimas gali būti naudojamas tokioms sistemoms kaip šifruoti protokolai, kombinuotos grandinės, skaitmeninės grandinės su vidine atmintimi ir programine įranga, išreikšta kaip pirminis kodas.

Šių sistemų verifikavimas vykdomas atliekant formalųjį patikrinimą abstrakčiam matematiniam sistemos moduliui, korespondenciją tarp matematinio modelio ir sistemos esmės, kitaip žinomos kaip konstrukcija. Matematinių objektų, dažnai naudojamų modeliuoti sistemas pavyzdžiai: baigtiniai struktūriniai mechanizmai, pažymėtos perėjimo sistemos, Petri tinklai, nustatyti automatai, hibridiniai automatai, procesinė algebra, formalios programavimo kalbų semantikos, kaip operacinės semantikos, denotacinės semantikos, aksiominės semantikos ir Hoare logika.

Formalaus verifikavo traktuotės[redaguoti | redaguoti vikitekstą]

Apytikriai yra du formalaus verifikavimo metodai.

Pirmas būdas yra modelio patikrinimas, kuris susideda iš sistematiškai nuodugnaus matematinio modelio patikrinimo (tai yra įmanoma baigtiniams modeliams, bet taip pat kai kuriems neribotiems modeliams, kuriuose neriboti būsenų komplektai gali būti efektyviai pateikti). Įprastai tai sudaro patikrinimas visų būsenų ir pereigų modelyje, naudojant greitą ir specifinę domeno abstrakcijos technikas apžiūrėti visas būsenų grupes per vieną operaciją ir sumažinti duomenų apdorojimo laiką. Į įgyvendinimo technikas įeina būsenos ploto enumeracija, simbolinė būsenos ploto enumeracija, abstrakto interpretacija, simbolinė simuliacija, abstrakcijos patobulinimas. Savybės, kurias reikia patikrinti, dažnai yra apibūdintos laikinose logikose, tokiose kaip linijinė laikinoji logika ar skaičiavimo medžio logika.

Antras būdas yra loginė interferencija. Tai sudaro naudojimas matematinio pagrindimo apie sistemą formalios versijos, įprastai naudojant teoremą išbandančią programinę įrangą, tokią kaip HOL teoremos bandytojas, ACL2, Isabelle, ar Coq teoremos bandytojus. Įprastai tai yra iš dalies automatizuota ir valdoma naudotojo supratimu sistemos, kurią reikia patvirtinti.

Validacija ir verifikavimas[redaguoti | redaguoti vikitekstą]

Verifikavimas yra vienas aspektas tikrinant produkto tinkamumą. Validacija yra papildomas aspektas. Dažnai minimas bendras tikrinimo procesas V ir V.

  • Validacija: „Ar mes bandome atlikti reikiamą dalyką? Ar produktas apibrėžia tikrus naudotojo poreikius?“
  • Verifikavimas: „Ar atlikome tai, ką bandėme atlikti? Ar produktas atitinka specifikacijas?“

Verifikavimo procesas susideda iš statiškų-struktūrinių ir dinaminių-elgesio aspektų. Pvz: programinės įrangos produktui galima tikrinti pirminį kodą (statišką) ir naudoti specifiniams tikrinimo atvejams (dinaminį). Validacija paprastai gali būti daroma tik dinamiškai, produktas testuojamas naudojant jį tipiškai ir netipiškai („Ar jis patenkinamai atlieka visus naudojimo atvejus?“)

Pramoninis naudojimas[redaguoti | redaguoti vikitekstą]

Dizaino sudėtingumo padidėjimas didina svarbą formalaus verifikavimo technikų programinės įrangos industrijoje. Šiomis dienomis formalioji verifikacija naudojama daugelio pirmaujančių techninės įrangos kompanijų, bet jos naudojimas programinės įrangos pramonėje yra vis dar apatiškas. Ši ypatybė gali būti priskiriama didesniam poreikiui techninės įrangos pramonėje, kur klaidos turi didesnę komercinę reikšmę. Dėl potencialių subtilių sąveikavimų tarp komponentų vis labiau sunku vykdyti realistinį galimybių komplektą naudojant simuliaciją. Svarbūs techninės įrangos aspektai yra atsakingi automatiniams tikrinimo metodams, palengvinant formalaus verifikavimo pristatymą ir jį padarant produktyvesnį.

2009 m. tik dvi operacinės sistemos yra formaliai patikrintos: Nicta Saugumo Įtvirtintas L4 mikrobranduolys ir Green Hills programinės įrangos integralumas (operacinė sistema)

Nuorodos[redaguoti | redaguoti vikitekstą]

  1. ^ http://www2.computer.org/portal/web/csdl/doi/10.1109/LICS.2003.1210044
  2. ^ http://portal.acm.org/citation.cfm?id=800667
  3. ^ Formal Verification in Industry
  4. ^ "A new OS has been proven to be correct using mathematical proofs. The cost: astronomical." by Jack Ganssle