În IT , la modelele de verificare sau modelul de verificare în limba engleză, este următoarea problemă: verifica dacă modelul unui sistem ( de multe ori de calculator sau electronic ) satisface o proprietate. De exemplu, vrem să verificăm dacă un program nu se blochează, dacă o variabilă nu este niciodată zero etc. De obicei proprietatea este scrisă într-un limbaj, adesea în logica temporală . Verificarea se face de obicei automat. Din punct de vedere practic, verificarea modelului a devenit, la nivel industrial, cea mai populară și mai utilizată metodă de verificare a codului și a sistemelor hardware de astăzi .
Verificarea modelelor se bazează pe logica temporală , unul dintre pionieri fiind Amir Pnueli , care a primit Premiul Turing în 1996 pentru „ [...] lucrare seminală care introduce logica temporală în știința calculatoare ” ( „[…] lucrări fundamentale care introduc logica temporală în informatică ” ). Verificarea modelului începe cu lucrările lui Edmund M. Clarke , E. Allen Emerson , Jean-Pierre Queille și Joseph Sifakis la începutul anilor 1980 Clarke, Emerson și Sifakis însuși au acordat Premiul Turing în 2007 pentru munca lor privind verificarea modelelor.
În această secțiune, specificăm ce înțelegem prin model și proprietate și apoi prin problema verificării modelului.
Sistemul este modelat de un sistem de tranziție de stat . Este un grafic direcționat : un vârf reprezintă o stare a sistemului și fiecare arc reprezintă o tranziție, adică o posibilă evoluție a sistemului de la o stare dată la o altă stare. Fiecare stat a graficului direcționat este marcat de setul de propozitii atomice adevărate la acel moment de execuție (de exemplu, i = 2 , procesorul 3 este în așteptare , etc. ). Un astfel de grafic se mai numește și o structură Kripke .
Exemplu de dozator de băuturiDăm aici exemplul unui dozator de băuturi care poate fi în 4 stări: așteptarea unei monede, selectarea unei băuturi, distribuirea unei sticle de apă minerală și distribuirea unei sticle de suc de portocale.
Exemplu de liftStarea sistemului este descrisă de nivelul actual al ascensorului între 0 și 3, starea apelurilor ( 4 butoane , câte unul pe etaj) și dacă ascensorul se deplasează și dacă patrulează în sus sau în jos. deci 4 × 2⁴ × 2 × 2 = 256 stări ).
Proprietatea care trebuie verificată este scrisă printr-o formulă logică temporală. De exemplu, dacă vrem să verificăm că x = 0 de un număr infinit de ori, putem scrie formula GF (x = 0) care citește „întotdeauna, în viitor, x = 0”. Distingem:
Dwyer și colab. a identificat 55 de tipuri de specificații în logica temporală liniară care apar în aplicații industriale.
Exemplu de dozator de băuturiDe exemplu, (GFa → (G (s → F (e sau j))) (dacă aparatul așteaptă un număr infinit de ori pentru o parte, atunci întotdeauna, de îndată ce este selectată o băutură, în viitor, o băutură (apă minerală sau suc de portocale) este livrat) este o adevărată proprietate pentru distribuitorul de băuturi.
Intrarea în problema de verificare a modelului este un model (de obicei un sistem de tranziție de stare) și o proprietate (de obicei scrisă în logică temporală). La ieșire, vrem să știm dacă proprietatea este verificată și, dacă da, un contraexemplu al unei execuții a sistemului care se modifică cu proprietatea.
Pentru proprietăți de siguranță (întotdeauna, p este fals), putem face o scanare aprofundată a graficului și putem verifica dacă fiecare stare îndeplinește p . Etichetarea algoritmilor există pentru logica temporală a arborelui (in) (CTL). Alte metode se bazează pe automate. Transformăm negarea formulei de verificat într-un automat și apoi facem produsul cartezian sincron cu automatul și modelul. Revenim apoi la testare dacă limbajul automatului produs este gol sau nu.
Navigarea în mod explicit (sau enumerarea) tuturor lumilor din structura lui Kripke poate fi costisitoare, motiv pentru care metodele simbolice, introduse de Ken McMillan și Ed Clarke, sunt mai relevante. O abordare, utilizată pe scară largă pentru verificarea proprietăților exprimate în logica arborelui temporal, se bazează pe reprezentarea simbolică a modelului. Au apărut multe metode de reprezentare a seturilor de state . Cel mai cunoscut folosește diagrame binare de decizie (BDD).
În loc să luăm în considerare ansamblul urmelor de execuție ale sistemului, ne putem limita la urmele finite, de lungime mărginită: aceasta este verificarea modelului mărginit . Existența unei urme care verifică o anumită proprietate este echivalentă cu satisfacția unei anumite formule booleene. Într-adevăr, dacă o stare a sistemului este descrisă printr-o k- tuplă booleană și suntem interesați de urmele de lungime mărginite de un anumit n, revenim la problema satisfacției unei formule propoziționale ( problema SAT ). Mai exact, dacă o formulă identifică stările inițiale ale sistemului, o formulă identifică stările a căror accesibilitate dorim să le testăm, iar o formulă este o relație de tranziție, atunci considerăm formula booleană unde sunt propoziții atomice care reprezintă starea la pas i de a rula sistemul. Există diverse programe software, numite rezolvatori SAT , care pot „efectiv în practică” să decidă problema SAT. În plus, acest software oferă de obicei un exemplu de evaluare care satisface formula succesului. Unele pot produce dovezi de insatisfacție în caz de eșec.
O dezvoltare recentă este adăugarea, pe lângă variabilele booleene, a variabilelor întregi sau reale. Formulele atomice nu mai sunt atunci doar variabile booleene, ci predicate atomice ale acestor variabile întregi sau reale, sau mai general predicate preluate dintr-o teorie (de exemplu , etc.). Vorbim apoi de satisfacția modulo-teoriei (de exemplu, putem considera egalitatea liniară și inegalitățile ca predicate atomice).
Modelul poate fi mai bogat decât automatele finite. De exemplu, există verificarea modelului pentru automatele temporizate . De asemenea, conceptul de verificare a modelului este generalizat în logica matematică. De exemplu, verificarea structurilor cu o formulă logică de prim ordin este PSPACE-complet; același lucru este valabil și pentru o formulă a logicii monadice de ordinul doi . Verificarea structurilor automate cu o formulă de prim ordin este decisă.
Tehnici precum Čegar ( contraexemplu ghidate Abstracție Refinement „rafinarea abstractizare ghidată de contra-exemple“) face posibilă transformarea unui program (scris în C , de exemplu) într - un model abstract apoi succesiv rafina modelul dacă este prea nepoliticos.
Există mai multe logici temporale: LTL, CTL, CTL * sau mu-calcul .
În sistemele cu mai mulți agenți , suntem interesați de proprietăți epistemice , cum ar fi „agentul știe că x = 0”, prin urmare, utilizarea logicii epistemice și a logicii care amestecă logica temporală și epistemică. Ne interesează raționarea despre existența strategiilor într-un joc : există logici pentru scrierea proprietăților pe jocuri precum „agentul are o strategie astfel încât într-o zi x = 0” ( logică temporală alternativă (în) ).
Din 2011, instrumentele care doresc acest lucru au participat la Concursul de verificare a modelelor (MCC), o competiție științifică internațională care permite compararea performanței „modelelor de verificare” pe diferite tipuri de calcule.
Un aspect important al cercetării verificării modelului este să demonstreze că o anumită clasă de proprietăți sau o anumită logică este decisivă sau că decizia sa aparține unei anumite clase de complexitate . Tabelul următor prezintă complexitatea verificării modelului pentru cele trei logici temporale LTL, CTL și CTL *. Cantitatea | M | este dimensiunea modelului reprezentat explicit. Cantitatea | φ | este dimensiunea specificației logice temporale. Complexitatea programului evaluează complexitatea verificării modelului atunci când formula de timp este fixată.
Logica temporală | Complexitatea timpului unui algoritm | Complexitatea verificării modelului | Complexitatea programului de verificare a modelului |
---|---|---|---|
LTL | O (| M | × 2 | φ | ) | PSPACE-complet | NLOGSPACE-complet |
CTL | O (| M | × | φ |) | P-complet | NLOGSPACE-complet |
CTL * | O (| M | × 2 | φ | ) | PSPACE-complet | NLOGSPACE-complet |
Orna Kupferman și Moshe Y. Vardi au introdus problema verificării modelelor sistemelor deschise, prescurtată ca verificare a modulelor . În verificarea modulelor, intrarea în problemă este un sistem de tranziție în care unele stări sunt controlate de sistemul în sine, iar altele sunt controlate de mediu. O proprietate temporală este adevărată într-un astfel de sistem de tranziție dacă este adevărată indiferent de alegerile mediului. Mai precis, având în vedere un sistem de tranziție M, considerăm desfășurarea lui V M , care este un copac infinit. O proprietate este adevărată în acest sistem dacă este adevărată în orice arbore obținut prin tăierea / eliminarea din V M a anumitor subarburi a căror rădăcină este succesorul unei stări controlate de mediu. Pentru verificarea modulelor, Orna Kupferman și Moshe Y. Vardi au arătat că complexitățile ating problema problemei de satisfacție în logica corespunzătoare:
Logica temporală | Complexitatea modulului de verificare | Complexitatea programului modulului de verificare |
---|---|---|
LTL | PSPACE-complet | NLOGSPACE-complet |
CTL | EXPTIME-complet | P-complet |
CTL * | 2EXPTIME-complet | P-complet |
Allur și colab. a studiat verificarea modelului cu o extensie a CTL și CTL * pentru a argumenta strategiile într-un sistem multi-agent. Tabelul următor prezintă rezultatele complexității pentru verificarea modelului pentru ATL și ATL *.
Logica temporală | Complexitatea verificării modelului | Complexitatea programului modulului de verificare |
---|---|---|
ATL | P-complet | NLOGSPACE-complet |
ATL * | 2EXPTIME-complet | P-complet |
După cum subliniază Allur și colab., Problema de verificare a modelului ATL * este apropiată de problema de sinteză LTL dezvoltată de Pnueli și Rosner, de asemenea 2EXPTIME-complete.
Un alt aspect al cercetării de verificare a modelului este găsirea algoritmilor eficienți în cazuri interesante în practică, implementarea lor și aplicarea lor la probleme reale.