I IT er verifikationsmodellerne eller modelkontrol på engelsk følgende problem: Kontroller, om modellen til et system (ofte computer eller elektronisk ) opfylder en ejendom. For eksempel vil vi kontrollere, at et program ikke går ned, at en variabel aldrig er nul osv. Normalt er ejendommen skrevet på et sprog, ofte i tidsmæssig logik . Verifikationen udføres normalt automatisk. Fra et praktisk synspunkt er modelbekræftelse på det industrielle niveau blevet den mest populære og udbredte metode til verifikation af kode- og hardwaresystemer i dag .
Verifikationen af modeller er baseret på tidsmæssig logik , hvoraf en af pionererne er Amir Pnueli , der modtog Turing-prisen i 1996 for ” […] seminal work introducing temporal logic into computing science ” ( “[…] fundamentale værker, der introducerer tidsmæssig logik i datalogi ” ). Den model kontrol begynder med arbejdet i Edmund M. Clarke , E. Allen Emerson , Jean-Pierre Queille og Joseph Sifakis i begyndelsen af 1980'erne Clarke, Emerson og Sifakis selv tildelt Turing Award i 2007 for deres arbejde med model kontrol.
I dette afsnit specificerer vi, hvad vi mener med model og egenskab og derefter med problemet med modelkontrol.
Systemet er modelleret af et statsovergangssystem . Det er en rettet graf : et toppunkt repræsenterer en tilstand af systemet, og hver bue repræsenterer en overgang, det vil sige en mulig udvikling af systemet fra en given tilstand til en anden tilstand. Hver tilstand orienteret graf er mærket ved sæt af atomare udsagn sandt ved dette punkt af programkode (f.eks i = 2 , processor 3 mangler , etc. ). En sådan graf kaldes også en Kripke-struktur .
Eksempel på drikkevaredispenserVi giver her eksemplet med en drikkedispenser, som kan være i 4 tilstande: venter på en mønt, vælger en drink, dispenserer en flaske mineralvand og dispenserer en flaske juicejuice.
Eksempel på elevatorenSystemets tilstand er beskrevet af det aktuelle niveau i elevatoren mellem 0 og 3, opkaldstilstanden ( 4 knapper , en pr. Etage), og hvis elevatoren bevæger sig, og om den patruljerer op eller ned. Lav (der er derfor er 4 × 2⁴ × 2 × 2 = 256 stater ).
Ejendommen, der skal kontrolleres, er skrevet med en tidsmæssig logisk formel. For eksempel, hvis vi vil kontrollere, at x = 0 et uendeligt antal gange, kan vi skrive formlen GF (x = 0), der lyder "altid i fremtiden, x = 0". Vi skelner mellem:
Dwyer et al. identificerede 55 typer specifikationer i lineær tidsmæssig logik, der vises i industrielle applikationer.
Eksempel på drikkevaredispenserFor eksempel (GFa → (G (s → F (e eller j))) (hvis maskinen venter et uendeligt antal gange på en del, så altid, så snart en drink er valgt, i fremtiden (mineralvand eller appelsinjuice) udstedes) er en sand ejendom for drikkevaredistributøren.
Input til modelkontrolproblemet er en model (typisk et tilstandsovergangssystem) og en egenskab (typisk skrevet i tidsmæssig logik). Som output ønsker vi at vide, om ejendommen er verificeret, og i bekræftende fald en modeksempel på en systemudførelse, der forstyrrer ejendommen.
Af sikkerhedsegenskaber (altid er p falsk) kan vi lave en dybdegående scanning af grafen og kontrollere, at hver tilstand opfylder p . Der findes mærkning af algoritmer til træets tidsmæssige logik (in) (CTL). Andre metoder er baseret på automater. Vi omdanner negationen af den formel, der skal kontrolleres, til en automat, og derefter gør vi det kartesiske produkt synkront med automaten og modellen. Vi vender derefter tilbage til at teste, om sproget i den producerede automat er tomt eller ej.
Eksplicit browsing (eller opregning) af alle verdener i Kripkes struktur kan være dyrt, hvorfor symbolske metoder, introduceret af Ken McMillan og Ed Clarke, er mere relevante. En tilgang, der er meget brugt til kontrol af egenskaber udtrykt i tidsmæssig trælogik, er baseret på den symbolske repræsentation af modellen. Der er opstået mange metoder til at repræsentere sæt af stater . Den bedst kendte bruger binære beslutningsdiagrammer (BDD).
I stedet for at overveje sæt af eksekveringsspor af systemet, kan vi begrænse os til begrænsede spor af afgrænset længde: dette er afgrænset modelkontrol . Eksistensen af et spor, der verificerer en bestemt egenskab, svarer til tilfredsstillelsen af en bestemt boolsk formel. Faktisk, hvis en tilstand af systemet beskrives af en boolsk k- tupper , og vi er interesseret i spor af længde afgrænset af en bestemt n, vender vi tilbage til problemet med tilfredsstillelsen af en propositionel formel ( problem SAT ). Mere præcist, hvis en formel identificerer systemets indledende tilstande, en formel identificerer de tilstande, hvis tilgængelighed vi vil teste, og en formel er en overgangsrelation, så betragter vi den boolske formel, hvor er atomforslag, der repræsenterer tilstanden ved trin jeg kører systemet. Der er forskellige softwareprogrammer, kaldet SAT-løsere , som "effektivt i praksis" kan afgøre SAT-problemet. Derudover giver denne software normalt et eksempel på en værdiansættelse, der opfylder formlen for succes. Nogle kan fremvise bevis for manglende tilfredshed i tilfælde af fiasko.
En nylig udvikling er tilføjelsen foruden boolske variabler af heltal eller reelle variabler. Atomiske formler er derefter ikke længere kun boolske variabler, men atomprædikater på disse heltal eller reelle variabler eller mere generelt prædikater taget fra en teori (for eksempel osv.). Vi taler derefter om tilfredshed modulo en teori (for eksempel kan vi betragte lineær lighed og uligheder som atomprædikater).
Modellen kan være rigere end endelige automater. For eksempel er der modelkontrol af tidsautomater . Begrebet modelkontrol er også generaliseret i matematisk logik. For eksempel er kontrol af strukturer med en førsteordens logikformel PSPACE-komplet; det samme gælder en formel for andenordens monadisk logik . Verifikationen af automatiske strukturer med en første ordres formel kan afgøres.
Teknikker såsom CEGAR ( Counterexample-Guided Abstraction Refinement , "refinement of abstraction guided by counter-examples") gør det muligt at omdanne et program (skrevet i C for eksempel) til en abstrakt model og derefter successivt forfine modellen, hvis den er for uhøflig.
Der er flere tidsmæssige logik: LTL, CTL, CTL * eller mu-calculus .
I multi-agentsystemer er vi interesserede i epistemiske egenskaber som “agenten ved, at x = 0”, derfor brugen af epistemisk logik og logik, der blander tidsmæssig og epistemisk logik. Vi er interesserede i at ræsonnere om eksistensen af strategier i et spil : der er logik til at skrive egenskaber på spil som "agenten har en strategi, så en dag x = 0" ( skiftevis tidsmæssig logik (in) ).
Siden 2011 har de værktøjer, der ønsker det, deltaget i Model Checking Contest (MCC), en international videnskabelig konkurrence, der gør det muligt at sammenligne udførelsen af "model checkers" på forskellige typer beregninger.
Et vigtigt aspekt af model kontrol forskning er at vise, at en bestemt klasse af egenskaber, eller en vis logik, er afgørbart , eller at dens afgørelse tilhører en bestemt klasse af kompleksitet . Den følgende tabel viser kompleksiteten af modelkontrol for de tre tidsmæssige logikker LTL, CTL og CTL *. Mængden | M | er størrelsen på modellen udtrykkeligt repræsenteret. Mængden | φ | er størrelsen på den tidsmæssige logiske specifikation. Programkompleksitet vurderer kompleksiteten af modelkontrol, når tidsformlen er fast.
Temporal logik | Tidskompleksitet af en algoritme | Kompleksitet af modelkontrol | Programkompleksitet af modelkontrol |
---|---|---|---|
LTL | O (| M | × 2 | φ | ) | PSPACE-komplet | NLOGSPACE-komplet |
CTL | O (| M | × | φ |) | P-komplet | NLOGSPACE-komplet |
CTL * | O (| M | × 2 | φ | ) | PSPACE-komplet | NLOGSPACE-komplet |
Orna Kupferman og Moshe Y. Vardi introducerede problemet med modelkontrol af åbne systemer, forkortet modulkontrol . Ved modulkontrol er indgangen til problemet et overgangssystem, hvor nogle stater styres af selve systemet, og andre styres af miljøet. En tidsmæssig egenskab er sand i et sådant overgangssystem, hvis det er sandt uanset miljøets valg. Mere præcist, givet et overgangssystem M, betragter vi dets udfoldning VM , som er et uendeligt træ. En egenskab er sand i dette system, hvis det er sandt i et hvilket som helst træ opnået ved beskæring / fjernelse fra V M visse undertræer, hvis rod er en efterfølger af en tilstand, der kontrolleres af miljøet. Til modulkontrol har Orna Kupferman og Moshe Y. Vardi vist, at kompleksiteten når op på tilfredshedsproblemet i de tilsvarende logikker:
Temporal logik | Kontrolmodulets kompleksitet | Kontrolmodulets kompleksitet |
---|---|---|
LTL | PSPACE-komplet | NLOGSPACE-komplet |
CTL | EXPTIME-komplet | P-komplet |
CTL * | 2EXPTIME-komplet | P-komplet |
Allur et al. studerede modelkontrol med en udvidelse af CTL og CTL * til at begrunde strategier i et multi-agent-system. Den følgende tabel giver kompleksitetsresultaterne til modelkontrol af ATL og ATL *.
Temporal logik | Kompleksitet af modelkontrol | Kontrolmodulets kompleksitet |
---|---|---|
ATL | P-komplet | NLOGSPACE-komplet |
ATL * | 2EXPTIME-komplet | P-komplet |
Som Allur et al. Påpeger, er problemet med ATL * -modelkontrol tæt på LTL-synteseproblemet udviklet af Pnueli og Rosner, også 2EXPTIME-komplet.
Et andet aspekt ved modelkontrol af forskning er at finde effektive algoritmer i interessante tilfælde i praksis, at implementere dem og anvende dem på reelle problemer.