Az informatikában az ellenőrzési modellek vagy az angol nyelvű modellellenőrzés a következő probléma: ellenőrizze, hogy egy rendszer (gyakran számítógépes vagy elektronikus ) modellje kielégít-e egy tulajdonságot. Például azt akarjuk ellenőrizni, hogy egy program nem zuhan-e össze, hogy egy változó soha nem nulla-e stb. Általában a tulajdonságot egy nyelven írják, gyakran időbeli logikában . Az ellenőrzés általában automatikusan történik. Gyakorlati szempontból a modellellenőrzés ipari szinten a legnépszerűbb és legelterjedtebb módszer a kód- és hardverrendszerek ellenőrzésére napjainkban .
A modellek ellenőrzése az időbeli logikán alapul , amelynek egyik úttörője Amir Pnueli , aki 1996-ban Turing-díjat kapott „ […] alapvető munkáért, amely az időbeli logikát bevezeti a számítástudományba ” ( „[…] alapművek, amelyek bemutatják a az időbeli logika a számítástechnikába ” ). A modell ellenőrzése kezdődik a munka Edmund M. Clarke , E. Allen Emerson , Jean-Pierre Queille és Joseph Sifakis az 1980 Clarke, Emerson és Sifakis magukat elnyerte a Turing-díjat , 2007-ben a munkájukért a modell ellenőrzése.
Ebben a részben meghatározzuk, mit értünk modell és tulajdonság, majd a modellellenőrzés problémája alatt.
A rendszert állapotátmenet rendszer modellezi . Ez egy irányított gráf : egy csúcs a rendszer állapotát, az egyes ívek pedig egy átmenetet jelentenek, vagyis a rendszer lehetséges alakulását egy adott állapotból egy másik állapotba. Minden állam a irányított gráf jelölt készlete által atomi kijelentések igaz ezen a ponton a végrehajtás (például, i = 2 , 3 processzor van folyamatban , stb ). Egy ilyen gráfot Kripke-struktúrának is neveznek .
Példa italadagolóraPéldát adunk egy italadagolóra, amely 4 állapotban lehet: érmére várni, italt választani, egy üveg ásványvizet és egy üveg gyümölcslé narancsot kiadni.
Példa a liftreA rendszer állapotát a lift aktuális szintje írja le 0 és 3 között, a hívások állapotát ( 4 gomb , emeletenként egy), és azt, hogy a lift mozog-e, és hogy felfelé vagy lefelé járőrözik-e. 4 × 2⁴ × 2 × 2 = 256 állapot ).
Az ellenőrizendő tulajdonságot egy időbeli logikai képlet írja. Például, ha azt akarjuk ellenőrizni, hogy x = 0 végtelen számú alkalommal, akkor megírhatjuk a GF (x = 0) képletet, amely "mindig, a jövőben x = 0" feliratú. Megkülönböztetünk:
Dwyer és mtsai. lineáris időbeli logikában 55 specifikációs típust azonosított, amelyek ipari alkalmazásokban jelennek meg.
Példa italadagolóraPéldául (GFa → (G (s → F (e vagy j))) (ha a gép végtelen sokszor vár egy alkatrészre, akkor mindig, amint egy italt választanak, a jövőben egy italt (ásványvizet vagy narancslevet szállítanak) igazi tulajdonság az italforgalmazó számára.
A modellellenőrzési probléma bemenete egy modell (általában állapotátmeneti rendszer) és egy tulajdonság (általában időbeli logikával írva). Kimenetként szeretnénk tudni, hogy a tulajdonság igazolva van-e, és ha igen, akkor egy ellenpélda egy olyan rendszerfuttatásról, amely megtapasztalja a tulajdonságot.
A biztonsági tulajdonságok (mindig, a p értéke hamis) érdekében elvégezhetjük a grafikon alapos beolvasását és ellenőrizhetjük, hogy minden állapot megfelel-e p-nek . Algoritmusok címkézése létezik a fa időbeli logikájához (in) (CTL). Más módszerek automatákon alapulnak. Az ellenőrizni kívánt képlet tagadását átalakítjuk automatává, majd szinkronba hozzuk a derékszögű szorzatot az automatával és a modellel. Ezután visszatérünk annak tesztelésére, hogy az előállított automatika nyelve üres-e vagy sem.
A Kripke felépítésében az összes világ kifejezett böngészése (vagy felsorolása) drága lehet, ezért a Ken McMillan és Ed Clarke által bevezetett szimbolikus módszerek relevánsabbak. Az egyik megközelítés, amelyet széles körben használnak az időbeli fa logikában kifejezett tulajdonságok ellenőrzésére, a modell szimbolikus ábrázolásán alapul. Az államhalmazok képviseletének számos módszere jelent meg . A legismertebb bináris döntési diagramokat (BDD) használ .
Ahelyett, hogy figyelembe vennénk a rendszer végrehajtási nyomainak halmazát, véges nyomokra korlátozódhatunk, korlátozott hosszúsággal: ez korlátozott modellellenőrzés . Egy bizonyos tulajdonságot igazoló nyom megléte egyenértékű egy bizonyos logikai képlet kielégíthetőségével. Valójában, ha a rendszer állapotát egy logikai k- példány írja le , és egy bizonyos n által határolt hosszúságú nyomok érdekelnek minket, akkor visszatérünk egy propozíciós képlet kielégíthetőségének problémájához ( SAT probléma ). Pontosabban, ha egy képlet azonosítja a rendszer kezdeti állapotait, egy képlet azonosítja azokat az állapotokat, amelyek hozzáférhetőségét tesztelni akarjuk, és egy képlet egy átmeneti reláció, akkor a Boole-képletet vesszük figyelembe, ahol vannak olyan atomtételek, amelyek a lépés állapotát képviselik i a rendszer futtatásáról. Különböző szoftverprogramok vannak, úgynevezett SAT megoldók , amelyek "hatékonyan képesek a gyakorlatban" eldönteni a SAT problémát. Ezenkívül ez a szoftver általában példát mutat az értékelésre, amely kielégíti a siker formuláját. Egyesek kudarc esetén bizonyítékot szolgáltathatnak az elégedetlenségre.
Egy újabb fejlemény a logikai változók mellett egész vagy valós változók hozzáadása. Az atomi képletek ekkor már nem csak logikai változók, hanem atom predikátumok ezekre az egész vagy valós változókra, vagy általánosabban egy elméletből vett predikátumokra (például stb.). Ezután modulo-elméleti kielégíthetőségről beszélünk (például a lineáris egyenlőséget és egyenlőtlenségeket tekinthetjük atomi predikátumoknak).
A modell gazdagabb lehet, mint a véges automaták. Például időzített automatákon van modellellenőrzés . A modellellenőrzés fogalmát a matematikai logika is általánosítja. Például a struktúrák elsőrendű logikai képlettel történő ellenőrzése PSPACE-teljes; ugyanez vonatkozik a másodrendű monádikus logika képletére is . Az automatikus struktúrák első rendű képlettel történő ellenőrzése eldönthető.
Az olyan technikák, mint a CEGAR ( Counterexample-Guided Abstraction Refinement , " absztrakció finomítása kontrapéldákkal vezérelve") lehetővé teszik egy program ( például C-ben írt ) absztrakt modellté való átalakítását, majd a modell egymást követő finomítását, ha túl durva.
Számos időbeli logika létezik: LTL, CTL, CTL * vagy mu-calculus .
A több ágenses rendszerekben olyan episztemikus tulajdonságok érdekelnek minket, mint például: „az ágens tudja, hogy x = 0”, ezért az episztémiás logikát és az időbeli és episztémiás logikát vegyítő logikákat alkalmazzák. Érdekelnek az érvelések a stratégiák létezéséről a játékban : léteznek logikák a tulajdonságok írásához a játékokon, például "az ügynöknek van egy stratégiája, hogy egy nap x = 0" ( váltakozó időbeli logika (be) ).
2011 óta az eszközök, amelyek ezt kívánják, részt vesznek a Nemzetközi Modellellenőrző Versenyen (MCC), amely egy nemzetközi tudományos verseny, amely lehetővé teszi a „modellellenőrök” teljesítményének összehasonlítását a különböző típusú számításoknál.
A modellellenőrzés kutatásának fontos szempontja annak demonstrálása, hogy a tulajdonságok bizonyos osztálya vagy egy bizonyos logikája eldönthető , vagy hogy döntése a komplexitás egy bizonyos osztályába tartozik . Az alábbi táblázat bemutatja a három időbeli logika LTL, CTL és CTL * modellellenőrzésének bonyolultságát. A mennyiség | M | a modell kifejezetten ábrázolt mérete. A mennyiség | φ | az időbeli logikai specifikáció mérete. A program bonyolultsága értékeli a modellellenőrzés összetettségét, amikor az idő képlete rögzített.
Időbeli logika | Egy algoritmus időbeli összetettsége | A modellellenőrzés összetettsége | A modellellenőrzés program bonyolultsága |
---|---|---|---|
LTL | O (| M | × 2 | φ | ) | PSPACE-teljes | NLOGSPACE-teljes |
CTL | O (| M | × | φ |) | P-teljes | NLOGSPACE-teljes |
CTL * | O (| M | × 2 | φ | ) | PSPACE-teljes | NLOGSPACE-teljes |
Orna Kupferman és Moshe Y. Vardi bemutatták a nyitott rendszerek modellellenőrzésének problémáját, rövidítve: modulellenőrzés . A modulellenőrzés során a probléma egy átmeneti rendszer, ahol egyes állapotokat maga a rendszer, másokat a környezet irányít. Az időbeli tulajdonság akkor igaz egy ilyen átmeneti rendszerben, ha a környezet választásaitól függetlenül igaz. Pontosabban, ha M átmeneti rendszert adunk, akkor annak kibontakozó V M- jét vesszük figyelembe , amely egy végtelen fa. Egy tulajdonság akkor igaz ebben a rendszerben, ha bármely olyan fára igaz, amelyet V M metszésével / eltávolításával nyernek egyes részfák, amelyek gyökere a környezet által irányított állapot utódja. A modulellenőrzéshez Orna Kupferman és Moshe Y. Vardi kimutatták, hogy a bonyolultságok elérik az elégedettség problémáját a megfelelő logikában:
Időbeli logika | Az ellenőrző modul összetettsége | Az ellenőrző modul program bonyolultsága |
---|---|---|
LTL | PSPACE-teljes | NLOGSPACE-teljes |
CTL | EXPTIME-teljes | P-teljes |
CTL * | 2EXPTIME-teljes | P-teljes |
Allur és mtsai. a CTL és a CTL * kiterjesztésével végzett modellellenőrzést tanulmányozta a multi-ágens rendszer stratégiáinak kifejtésére. Az alábbi táblázat az ATL és az ATL * modellellenőrzésének összetettségét mutatja be.
Időbeli logika | A modellellenőrzés összetettsége | Az ellenőrző modul program bonyolultsága |
---|---|---|
ATL | P-teljes | NLOGSPACE-teljes |
ATL * | 2EXPTIME-teljes | P-teljes |
Mint Allur és munkatársai rámutatnak, az ATL * modellellenőrzési probléma közel áll a Pnueli és Rosner által kifejlesztett LTL szintézis problémához, szintén 2EXPTIME-teljes.
A modellellenőrzés kutatásának másik szempontja az , hogy hatékony algoritmusokat találjon a gyakorlatban érdekes esetekről, ezeket megvalósítsa és valós problémákra alkalmazza.