V IT představují ověřovací modely nebo kontrola modelu v angličtině následující problém: zkontrolujte, zda model systému (často počítačového nebo elektronického ) vyhovuje vlastnosti. Chceme například zkontrolovat, zda program nespadne, zda proměnná není nikdy nula atd. Vlastnost je obvykle napsána v jazyce, často v časové logice . Ověření se obvykle provádí automaticky. Z praktického hlediska se ověření modelu stalo na průmyslové úrovni nejoblíbenější a nejrozšířenější metodou ověřování kódových a hardwarových systémů současnosti .
Ověření modelů je založeno na časové logice , jejímž jedním z průkopníků je Amir Pnueli , který v roce 1996 obdržel Turingovu cenu za „ […] klíčovou práci zavádějící časovou logiku do počítačové vědy “ ( „[...] základní práce, které zavádějí časová logika do informatiky “ ). Kontrola modelu začíná prací Edmunda M. Clarka , E. Allena Emersona , Jean-Pierre Queille a Josepha Sifakise na začátku 80. let, kdy Clarke, Emerson a Sifakis sami ocenili Turingovu cenu v roce 2007 za práci na kontrole modelu.
V této části určíme, co máme na mysli modelem a vlastností a poté problémem kontroly modelu.
Systém je modelován systémem přechodu stavu . Jedná se o směrovaný graf : vrchol představuje stav systému a každý oblouk představuje přechod, to znamená možný vývoj systému z daného stavu do jiného stavu. Každý stav orientovaného grafu je označen souborem atomových tvrzení pravdivé v tomto místě provádění (například, i = 2 , procesor 3 čeká , atd. ). Takový graf se také nazývá struktura Kripke .
Příklad automatu na nápojeUvádíme zde příklad výdejníku nápojů, který může být ve 4 stavech: čekání na minci, výběr nápoje, výdej lahve minerální vody a výdej lahve pomerančové šťávy.
Příklad výtahuStav systému je popsán aktuální úrovní výtahu mezi 0 a 3, stavem hovorů ( 4 tlačítka , jedno na patře) a tím, zda se výtah pohybuje a zda hlídá nahoru nebo dolů. Nízká (existují tedy 4 × 2⁴ × 2 × 2 = 256 stavů ).
Vlastnost, která má být zkontrolována, je zapsána časovým logickým vzorcem. Například pokud chceme zkontrolovat, že x = 0 nekonečně mnohokrát, můžeme napsat vzorec GF (x = 0), který zní „vždy, v budoucnu x = 0“. Rozlišujeme:
Dwyer a kol. identifikovalo 55 typů specifikací v lineární časové logice, které se objevují v průmyslových aplikacích.
Příklad automatu na nápojeNapříklad, (GFa → (G (s → F (e nebo j)))) (pokud stroj čeká nekonečně mnohokrát na součást, pak vždy, jakmile je vybrán nápoj, v budoucnu nápoj (minerální voda nebo pomerančový džus) je skutečným majetkem distributora nápojů.
Vstupem do problému kontroly modelu je model (obvykle systém přechodu stavu) a vlastnost (obvykle napsaná v časové logice). Na výstupu chceme vědět, zda je vlastnost ověřena, a pokud ano, protiklad provedení systému, který s touto vlastností naráží.
U bezpečnostních vlastností (vždy, p je nepravdivé) můžeme provést hloubkový sken grafu a zkontrolovat, zda každý stav splňuje p . Označení algoritmů existuje pro stromovou dočasnou logiku (in) (CTL). Další metody jsou založeny na automatech. Transformujeme negaci vzorce, který má být zkontrolován, do automatu a poté synchronizujeme kartézský součin s automatem a modelem. Poté se vrátíme k testování, zda je jazyk produkovaného automatu prázdný nebo ne.
Explicitní procházení (nebo výčet) všech světů ve struktuře Kripkeho může být nákladné, a proto jsou důležitější symbolické metody zavedené Kenem McMillanem a Edem Clarkem . Jeden přístup, široce používaný pro kontrolu vlastností vyjádřených v logice časových stromů, je založen na symbolické reprezentaci modelu. Objevilo se mnoho metod reprezentace množin států . Nejznámější používá binární rozhodovací diagramy (BDD).
Místo toho, abychom zvážili množinu tras popravy systému, můžeme se omezit na konečné stopy omezené délky: toto je kontrola omezeného modelu . Existence stopy ověřující určitou vlastnost je ekvivalentní s uspokojivostí určitého booleovského vzorce. Ve skutečnosti, pokud je stav systému popsán booleovskými k -tuples a nás zajímají stopy délky ohraničené určitým n, vrátíme se k problému uspokojivosti výrokového vzorce ( problém SAT ). Přesněji řečeno, pokud vzorec identifikuje počáteční stavy systému, vzorec identifikuje stavy, jejichž přístupnost chceme testovat, a vzorec je přechodovým vztahem, pak uvažujeme booleovský vzorec, kde jsou atomové výroky, které představují stav v kroku i spuštění systému. Existují různé softwarové balíčky zvané SAT solvers , které mohou „efektivně v praxi“ rozhodnout o problému SAT. Kromě toho tento software obvykle poskytuje příklad ocenění, které splňuje vzorec úspěchu. Některé mohou v případě selhání předložit důkazy o neuspokojivosti.
Nedávný vývoj je přidání, kromě booleovských proměnných, celočíselných nebo skutečných proměnných. Atomové vzorce již nejsou jen booleovské proměnné, ale atomové predikáty těchto celočíselných nebo reálných proměnných nebo obecněji predikáty převzaté z teorie (například atd.). Mluvíme pak o uspokojivosti modulo-teorie (například můžeme považovat lineární rovnost a nerovnosti za atomové predikáty).
Model může být bohatší než konečné automaty. Například existuje kontrola modelu na časovaných automatech . Koncept kontroly modelu je také zobecněn v matematické logice. Například kontrola struktur pomocí logického vzorce prvního řádu je úplná PSPACE; totéž platí pro vzorec monadické logiky druhého řádu . Ověření automatických struktur pomocí vzorce prvního řádu je rozhodné.
Techniky jako CEGAR (Counterexample -Guided Abstraction Refinement , „refinement of abstraction guided by counter-examples“) umožňují transformovat program (napsaný například v jazyce C ) do abstraktního modelu a poté postupně vylepšovat model, pokud je příliš hrubý.
Existuje několik časových logik: LTL, CTL, CTL * nebo mu-kalkul .
V systémech s více agenty se zajímáme o epistemické vlastnosti, jako je „agent ví, že x = 0“, proto použití epistemické logiky a logik, které kombinují časovou a epistemickou logiku. Zajímají nás úvahy o existenci strategií ve hře : existují logické vlastnosti pro psaní her, například „agent má strategii tak, že jednoho dne x = 0“ ( časová logika střídavého času (in) ).
Od roku 2011 se nástroje, které si to přejí, účastní soutěže Model Checking Contest (MCC), mezinárodní vědecké soutěže, která umožňuje porovnávat výkonnost „model checkers“ na různých typech výpočtů.
Důležitým aspektem výzkumu kontroly modelu je prokázat, že určitá třída vlastností nebo určitá logika je rozhodnutelná nebo že její rozhodnutí patří do určité třídy složitosti . Následující tabulka ukazuje složitost kontroly modelu pro tři časové logiky LTL, CTL a CTL *. Množství | M | je velikost modelu výslovně znázorněna. Množství | φ | je velikost specifikace časové logiky. Složitost programu hodnotí složitost kontroly modelu, když je časový vzorec pevný.
Časová logika | Časová složitost algoritmu | Složitost kontroly modelu | Programová složitost kontroly modelu |
---|---|---|---|
LTL | O (| M | × 2 | φ | ) | PSPACE - kompletní | NLOGSPACE - kompletní |
CTL | O (| M | × | φ |) | P-kompletní | NLOGSPACE - kompletní |
CTL * | O (| M | × 2 | φ | ) | PSPACE - kompletní | NLOGSPACE - kompletní |
Orna Kupferman a Moshe Y. Vardi představili problém kontroly modelu otevřených systémů, zkráceně jako kontrola modulu . Při kontrole modulu je vstupem do problému přechodový systém, kde některé stavy jsou řízeny samotným systémem a jiné jsou ovládány prostředím. Časová vlastnost je v takovém přechodovém systému pravdivá, pokud je pravdivá bez ohledu na výběr prostředí. Přesněji řečeno, vzhledem k přechodovému systému M uvažujeme jeho rozvíjející se V M , což je nekonečný strom. Vlastnost je v tomto systému pravdivá, pokud je pravdivá v každém stromu získaném prořezáváním / odebíráním z V M určitých podstromů, jejichž kořen je nástupcem stavu ovládaného prostředím. Pro kontrolu modulů ukázaly Orna Kupferman a Moshe Y. Vardi, že složitosti dosahují složitosti problému uspokojivosti v odpovídajících logikách:
Časová logika | Složitost kontrolního modulu | Složitost programu kontrolního modulu |
---|---|---|
LTL | PSPACE - kompletní | NLOGSPACE - kompletní |
CTL | EXPTIME - kompletní | P-kompletní |
CTL * | 2EXPTIME - kompletní | P-kompletní |
Allur a kol. studoval kontrolu modelu s rozšířením CTL a CTL *, aby uvažoval o strategiích v systému s více agenty. Následující tabulka poskytuje výsledky složitosti pro kontrolu modelu na ATL a ATL *.
Časová logika | Složitost kontroly modelu | Složitost programu kontrolního modulu |
---|---|---|
ATL | P-kompletní | NLOGSPACE - kompletní |
ATL * | 2EXPTIME - kompletní | P-kompletní |
Jak upozorňují Allur a kol., Problém kontroly modelu ATL * je blízký problému syntézy LTL vyvinutému Pnueli a Rosnerem, také 2EXPTIME-complete.
Dalším aspektem výzkumu kontroly modelu je najít efektivní algoritmy pro zajímavé případy v praxi, implementovat je a aplikovat na skutečné problémy.