Verificare formală
În contextul sistemelor software și hardware, verificarea formală este acțiunea de a dovedi matematic sau de a contesta corectitudinea algoritmilor unui sistem prin verificarea respectării formalităților sau proprietăților specifice, folosind metode matematice formale . [1]
Este util pentru asigurarea corectitudinii sistemelor precum: protocoale criptografice, circuite combinaționale , circuite digitale cu memorie internă și software exprimat în cod sursă.
Verificarea acestor sisteme se face prin furnizarea unei dovezi formale a unui model matematic abstract al sistemului, corespondența dintre modelul matematic și natura sistemului este cunoscută încă de la construcția sa. În modele se folosesc de obicei: mașina cu stări finite , sistemul de stare de tranziție , rețeaua Petri , sistemul vectorial suplimentar, teoria automată temporizată, teoria automatelor hibride, calculul algebric, semantica formală a limbajelor de programare precum semantica operațională, semantica denotațională, semantica axiomatică și logica lui Hoare . [2]
Uz comercial
Notă
- ^ Alok Sanghavi, Ce este verificarea formală? , în EE Times_Asia , 21 mai 2010.
- ^ Introducere în verificarea formală , Universitatea Berkeley din California, Accesat la 6 noiembrie 2013