Modelių tikrinimas

Straipsnis iš Vikipedijos, laisvosios enciklopedijos.
Peršokti į: navigaciją, paiešką
 Broom icon.svg  Šį puslapį ar jo dalį reikia sutvarkyti pagal Vikipedijos standartus.
Jei galite, sutvarkykite; apie sutvarkymą galite pranešti specialiame Vikipedijos projekte.
 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.

Modelių tikrinimu informatikoje vadinamas automatizuotas patikrinimas, ar modelis atitinka pateiktus reikalavimus. Dažniausiai tai programinės ar techninės įrangos sistemos (nebūtinai), ir dažniausi reikalavimai yra aklaviečių ar panašių kritinių būsenų, lemiančių blogą sistemos, nebuvimas.


Ši užduotis sprendžiama užrašant sistemos modelį ir reikalavimus matematine kalba (t. y., užrašant jų formalias specifikacijas, ir tada patikrinant ar sistema tenkina reikalavimą užrašytą kaip loginę formulę. Toks būdas yra bendras ir gali būti taikomas visų tipų [Logika|logikoms]. Paprasta modelių tikrinimo problema yra patikrinimas, ar duota teiginių logikos formulė yra tenkinama sistemos modelio.

Apžvalga[taisyti | redaguoti kodą]

Svarbūs modelio patikrinimo metodai buvo sukurti, kad jų pagalba būtų galima patikrinti techninės įrangos ir programinės įrangos modelius, kuriuose reikalavimai yra išreikšti laikinos loginės formulės pagalba. Novatoriškas laikinos loginės formulės modelio patikrinimo darbas buvo sukurtas E. M. Clarke ir E. A. Emerson bei J. P. Queille ir J. Sifakis. Clarke, Emerson ir Sifakis gavo bendrą Turing apdovanojimą už jų darbą modelio patikrinimo srityje. Modelio patikrinimas yra dažniausiai naudojamas patikrinant techninės įrangos modelį. Dirbant su programine įranga dėl netikrumo (žiūrėkite apskaičiavimo teoriją) metodas negali būti pilnai algoritminis; paprastai jis gali nepatvirtinti arba klaidingai patvirtinti reikiamą savybę. Struktūra paprastai yra suvokiama kaip pirminis kodinis apibūdinimas, išreikštas pramonine techninės įrangos aprašomąja kalba arba specialios paskirties kalba. Tokia programa atitinka ribotos būsenos mašiną (FSM), pvz., adresuotoje grafoje yra mazgai (arba viršūnės) ir briaunos. Atominių teiginių grupė yra susijusi su kiekvienu mazgu, paprastai rodo, kurie atminties elementai yra įjungti. Mazgai reiškia sistemos būsenas, briaunos reiškia galimus perėjimus, kurie gali keisti būseną, tuo tarpu atominiai teiginiai išreiškia esmines savybes, kurios užtikrina darbo eigą. Paprastai, problema gali būti išreiškiama taip: turime norimą savybę, išreikštą kaip laikiną logišką formulę p, ir struktūra M su pirmine būsena s, apskaičiuokite, ar M, sI= p. Jei M yra galutinė, kaip yra techninėje įrangoje, modelio patikrinimas susiaurėja iki grafos paieškos.

Modelio patikrinimo priemonės[taisyti | redaguoti kodą]

Modelio patikrinimo priemonės susiduria su kombinatoriniu erdviniu sprogimu, kuris plačiai žinomas kaip būsenos sprogimo problema, kuri turi būti taikoma sprendžiant daugumą realaus pasaulio problemų. Egzistuoja keli būdai, kaip spręsti šią problemą.

  1. Simboliniai algoritmai neleidžia kurti grafos FSM; vietoj to jie išreiškia grafą netiesiogiai, naudojant formulę teiginių logikoje. Dvigubo sprendimo diagramos (BDD) naudojimas buvo išpopuliarintas dėka Ken McMillan darbo.
  2. Riboti modelio patikrinimo algoritmai atskleidžia FSM per tam tikrą skaičių ėjimų k ir leidžia patikrinti, ar savybės pažeidimas gali įvykti būnant k arba einant per mažiau ėjimų. Tai paprastai apima ribojamo modelio kodavimą, kas reiškia SAT pradžią. Procesas gali būti kartojamas, naudojant vis didesnes ir didesnes k reikšmes, kol visi galimi pažeidimai bus pašalinti (palyginkite pasikartojantis gilėjantis gylio ieškojimas).
  3. Dalinis nurodymo sumažinimas gali būti naudojamas (detalioje grafoje), kad būtų galima sumažinti konkurencingo proceso atskirų įtarpų skaičių. Esminė idėja yra ta, kad jei yra nesvarbu, ar A arba B yra vykdomas pirmiausiai, tada tai tėra laiko švaistymas, norint apsvarstyti AB ir BA įtarpus.
  4. Abstrakcija yra skirta siekiant patvirtinti sistemos savybes, pirmiausiai ją supaprastinant. Supaprastinta sistema paprastai neatitinka tų pačių savybių, kokias turi pirminė sistema, todėl gali būti būtina įvykdyti tobulinimo procesą. Paprastai vienoje sistemoje reikalinga garso išraiška (savybės, kurios yra pagrįstos išraiškomis, yra tokios pačios, kaip ir pirminėje sistemoje); tačiau dažniausiai išraiška nėra išbaigta (ne visos pirminės sistemos tikrosios savybės gali būti išreiškiamos). Programoje išraiškos pavyzdys būtų pvz., ignoruoti loginės algebros kintamųjų reikšmes ir atsižvelgti tik į loginės algebros kintamuosius bei kontroliuoti programinį srautą; tokia išraiška, jei ji gali būti prasta, tiesą sakant gali būti tinkama, norint įrodyti, pvz., bendro išskyrimo savybes.
  5. Apskaičiuojamosios išraiškos tobulinimas (CEGAR) prasideda nuo tikrinimo dėl prastos išraiškos (netinkamos) ir pasikartojančiai gryninant ją. Kai pažeidimas (skaičiavimo) yra nustatomas, priemonė ima analizuoti jį (pvz., ar pažeidimas yra tikras ar tik neužbaigtos išraiškos rezultatas). Jei pažeidimas yra tikras, apie tai pranešama naudotojui; jei ne, operacija, įrodanti, kad pažeidimas netikras, naudojama norint pagerinti išraišką ir patikrinimas pradedamas iš naujo.

Modelio patikrinimo įrankiai buvo pradžioje sukurti tam, kad jų pagalba būtų galima pagrįsti loginį abstrakčios būsenos sistemų teisingumą, bet jie buvo ištobulinti, kad būtų galima dirbti su savalaikėmis ir ribotų formų hibridinėmis sistemomis.

Papildoma medžiaga[taisyti | redaguoti kodą]

Priemonės

  • BLAST modelio tikrintuvas
  • CADP (Išplėtotų procesų konstrukcija ir analizė) priemonių rinkinys komunikaciniams protokolams ir išplėtotoms sistemoms kurti
  • CHIC
  • CHESS modelis
  • ISP kodo lygmens tikrintojas dirbant su MPI programomis
  • Java Pathfinder- atviras modelio tikrintojas dirbant su Java programomis
  • Moon Walker- atviras pirminio modelio tikrintojas dirbant su NET programomis
  • Markov Reward Modelio tikrintojas (MRMC)
  • NuSMV, naujas simbolinis modelio tikrintojas
  • PRISM (modelio tikrintojas), tikimybinis simbolių modelio tikrintojas
  • Rabbit
  • SPIN modelio tikrintojas, bendra priemonė, padedanti patvirtinti išplėtotų programinės įrangos modelių teisingumą tiksliai ir automatizuotai
  • Vereofy: [1]: programinės įrangos modelio tikrintojas, dirbant su sudedamųjų dalių sistemomis, kad būtų pasiektas operacinis tikslumas
  • µCRL
  • mCRL2
  • UPPAAL integruota priemonių aplinka modeliavimui, patvirtinimui ir patikrinimui, dirbant su savalaikėmis sistemomis, sukurtomis kaip laiku pagristų automatų tinklas

Susijusios technikos

  • Abstrakti interpretacija
  • Automatinis teoremos įrodymas
  • Programos analizė (kompiuterių mokslas)
  • Statinė kodo analizė

Nuorodos[taisyti | redaguoti kodą]

  1. ^ Allen Emerson, E.; Clarke, Edmund M. (1980), "Characterizing correctness properties of parallel programs using fixpoints", Automata, Languages and Programming, doi:10.1007/3-540-10003-2_69
  2. ^ Edmund M. Clarke, E. Allen Emerson: "Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic". Logic of Programs 1981: 52-71.
  3. ^ Clarke, E. M.; Emerson, E. A.; Sistla, A. P. (1986), "Automatic verification of finite-state concurrent systems using temporal logic specifications", ACM Transactions on Programming Languages and Systems 8: 244, doi:10.1145/5397.5399
  4. ^ Queille, J. P.; Sifakis, J. (1982), "Specification and verification of concurrent systems in CESAR", International Symposium on Programming, doi:10.1007/3-540-11494-7_22
  5. ^ Press Release: ACM Turing Award Honors Founders of Automatic Verification Technology
  6. ^ USACM: 2007 Turing Award Winners Announced
  7. ^ * Symbolic Model Checking, Kenneth L. McMillan, Kluwer, ISBN 0-7923-9380-5, also online.
  8. ^ Clarke, Edmund; Grumberg, Orna; Jha, Somesh; Lu, Yuan; Veith, Helmut (2000), "Counterexample-Guided Abstraction Refinement", Computer Aided Verification 1855: 154, doi:10.1007/10722167_15