Verificació formal
En el context dels sistemes de maquinari i programari, la verificació formal és l'acte de demostrar o desmentir la correcció d'un sistema respecte a una determinada especificació o propietat formal, utilitzant mètodes formals matemàtics.[1] La verificació formal és un incentiu clau per a l'especificació formal dels sistemes, i és el nucli dels mètodes formals. Representa una dimensió important de l'anàlisi i la verificació en l'automatització del disseny electrònic i és un enfocament de la verificació de programari. L'ús de la verificació formal permet obtenir el més alt nivell de garantia d'avaluació (EAL7) en el marc de criteris comuns per a la certificació de seguretat informàtica
La verificació formal pot ser útil per demostrar la correcció de sistemes com ara: protocols criptogràfics, circuits combinacionals, circuits digitals amb memòria interna i programari expressat com a codi font en un llenguatge de programació. Exemples destacats de sistemes de programari verificats inclouen el compilador C verificat CompCert i el nucli del sistema operatiu d'alta seguretat seL4.
La verificació d'aquests sistemes es fa assegurant l'existència d'una demostració formal d'un model matemàtic del sistema.[2] Exemples d'objectes matemàtics utilitzats per modelar sistemes són: màquines d'estats finits, sistemes de transició etiquetats, clàusules de Horn, xarxes de Petri, sistemes d'addició vectorial, autòmats cronometrats, autòmats híbrids, àlgebra de processos, semàntica formal de llenguatges de programació com la semàntica operacional, semàntica denotacional i semàntica axiomàtica axiomàtica.
Aproximacions
[modifica]Comprovació de models
[modifica]La verificació de models implica una exploració sistemàtica i exhaustiva del model matemàtic. Aquesta exploració és possible per als models finits, però també per a alguns models infinits, on els conjunts infinits d'estats es poden representar eficaçment de manera finita utilitzant l'abstracció o aprofitant la simetria. Normalment, això consisteix a explorar tots els estats i transicions del model, mitjançant l'ús de tècniques d'abstracció intel·ligents i específiques de domini per considerar grups sencers d'estats en una única operació i reduir el temps de càlcul. Les tècniques d'implementació inclouen l'enumeració d'espais d'estats, l'enumeració simbòlica d'espais d'estats, la interpretació abstracta, la simulació simbòlica i el perfeccionament de l'abstracció. Les propietats que s'han de verificar es descriuen sovint en lògiques temporals, com ara la lògica temporal lineal (LTL), el llenguatge d'especificació de propietats (PSL), les assercions SystemVerilog (SVA),[3] o la lògica d'arbre computacional (CTL). El gran avantatge de la comprovació de models és que sovint és totalment automàtica; el seu principal desavantatge és que no s'adapta en general a grans sistemes; Els models simbòlics solen estar limitats a uns quants centenars de bits d'estat, mentre que l'enumeració d'estats explícita requereix que l'espai d'estat que s'està explorant sigui relativament petit.
Verificació deductiva
[modifica]Un altre enfocament és la verificació deductiva.[4][5] Consisteix a generar a partir del sistema i les seves especificacions (i possiblement altres anotacions) una col·lecció d' obligacions de demostració matemàtica, la veritat de les quals implica la conformitat del sistema amb la seva especificació, i acomplir aquestes obligacions mitjançant assistents de demostració (provadors interactius de teoremes) (com HOL, ACL2, Isabelle, Rocq), els coneguts anteriorment com a PVS o automàtics (anteriorment). incloent, en particular, els solucionadors de teories de mòdul de satisfaciabilitat (SMT). Aquest enfocament té l'inconvenient que pot requerir que l'usuari entengui detalladament per què el sistema funciona correctament, i transmetre aquesta informació al sistema de verificació, ja sigui en forma d'una seqüència de teoremes a demostrar o en forma d'especificacions (invariants, precondicions, postcondicions) dels components del sistema (per exemple, funcions o procediments) i potser subcomponents (per exemple, estructures de dades o bucles).
Aplicació al programari
[modifica]La verificació formal dels programes de programari implica demostrar que un programa compleix una especificació formal del seu comportament. Les subàrees de la verificació formal inclouen la verificació deductiva (vegeu més amunt), la interpretació abstracta, la demostració automatitzada de teoremes, els sistemes de tipus i els mètodes formals lleugers. Un enfocament de verificació basat en tipus prometedor és la programació de tipus depenent, en què els tipus de funcions inclouen (almenys una part de) les especificacions d'aquestes funcions, i la verificació de tipus del codi estableix la seva correcció amb aquestes especificacions. Els idiomes escrits depenentment amb totes les funcions admeten la verificació deductiva com a cas especial.
Un altre enfocament complementari és la derivació de programes, en què el codi eficient es produeix a partir d'especificacions funcionals mitjançant una sèrie de passos per preservar la correcció. Un exemple d'aquest enfocament és el formalisme Bird-Meertens, i aquest enfocament es pot veure com una altra forma de síntesi de programes.
Aquestes tècniques poden ser sòlides, és a dir, que les propietats verificades es poden deduir lògicament de la semàntica, o poc sòlides, el que significa que no hi ha aquesta garantia. Una tècnica sòlida només dóna un resultat quan ha cobert tot l'espai de possibilitats. Un exemple de tècnica no adequada és aquella que cobreix només un subconjunt de possibilitats, per exemple només nombres enters fins a un nombre determinat, i dóna un resultat "prou bo". Les tècniques també poden ser decidibles, el que significa que es garanteix que les seves implementacions algorítmiques acaben amb una resposta, o indecidibles, és a dir, que mai no s'acaben. En limitar l'abast de les possibilitats, es podrien construir tècniques no sòlides que siguin decidibles quan no hi hagi tècniques de so determinables disponibles.
Verificació i validació
[modifica]La verificació és un aspecte de la prova de l'adequació d'un producte per al seu propòsit. La validació és l'aspecte complementari. Sovint es fa referència al procés de comprovació global com a V i V.
- Validació : "Estem intentant fer el correcte?", és a dir, el producte s'especifica a les necessitats reals de l'usuari?
- Verificació : "Hem fet el que estàvem intentant fer?", és a dir, el producte s'ajusta a les especificacions?
El procés de verificació consta d'aspectes estàtics/estructurals i dinàmics/conductuals. Per exemple, per a un producte de programari es pot inspeccionar el codi font (estàtic) i executar-se amb casos de prova específics (dinàmics). Normalment, la validació només es pot fer de forma dinàmica, és a dir, el producte es prova mitjançant usos típics i atípics ("Compleix satisfactòriament tots els casos d'ús ?").
Reparació automatitzada de programes
[modifica]La reparació del programa es realitza respecte a un oracle, que inclou la funcionalitat desitjada del programa que s'utilitza per validar la correcció generada. Un exemple senzill és una suite de proves: els parells d'entrada/sortida especifiquen la funcionalitat del programa. S'utilitzen una varietat de tècniques, sobretot utilitzant solucionadors de teories de mòduls de satisfacció (SMT) i programació genètica,[6] utilitzant la computació evolutiva per generar i avaluar possibles candidats per a correccions. El primer mètode és determinista, mentre que el segon és aleatoritzat.
La reparació de programes combina tècniques de verificació formal i síntesi de programes. Les tècniques de localització d'errors en la verificació formal s'utilitzen per calcular punts del programa que podrien ser possibles localitzacions d'errors, que poden ser orientats pels mòduls de síntesi. Els sistemes de reparació sovint se centren en una petita classe d'errors predefinida per tal de reduir l'espai de cerca. L'ús industrial és limitat a causa del cost computacional de les tècniques existents.
Ús industrial
[modifica]El creixement de la complexitat dels dissenys augmenta la importància de les tècniques de verificació formal en la indústria del maquinari.[7] En l'actualitat, la verificació formal és utilitzada per la majoria o per a totes les empreses de maquinari líders,[8] però el seu ús a la indústria del programari encara està llanguit. Això es podria atribuir a la major necessitat de la indústria del maquinari, on els errors tenen una importància comercial més gran. A causa de les possibles interaccions subtils entre components, és cada cop més difícil exercir un conjunt realista de possibilitats mitjançant la simulació. Aspectes importants del disseny de maquinari són susceptibles de mètodes de prova automatitzats, cosa que fa que la verificació formal sigui més fàcil d'introduir i més productiva.[9]
Referències
[modifica]- ↑ Sanghavi, Alok EE Times Asia, 21-05-2010.
- ↑ Sanjit A. Seshia. «Chapter 3: Modeling for Verification». A: Clarke, Edmund M.. Handbook of Model Checking (en anglès). Springer, 2018, p. 75–105. DOI 10.1007/978-3-319-10575-8. ISBN 978-3-319-10574-1.
- ↑ Cohen, Ben. SystemVerilog Assertions Handbook (en anglès). 4th. CreateSpace Independent Publishing Platform, 2015. ISBN 978-1518681448.
- ↑ Ahrendt. Deductive Software Verification - The KeY Book: From Theory to Practice (en anglès). 1st 2016. Cham: Springer International Publishing : Imprint: Springer, 2016. ISBN 978-3-319-49812-6.
- ↑ «Building Deductive Program Verifiers - Lecture Notes». A: Pretschner. Engineering secure and dependable software systems (en anglès). Amsterdam, Netherlands: IOS Press, 2019. ISBN 978-1-61499-976-8.
- ↑ Le Goues, Claire; Nguyen, ThanhVu; Forrest, Stephanie; Weimer, Westley IEEE Transactions on Software Engineering, 38, 1, 1-2012, pàg. 54–72. DOI: 10.1109/TSE.2011.104.
- ↑ Harrison, J. «Formal verification at Intel». A: 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings (en anglès), 2003, p. 45–54. DOI 10.1109/LICS.2003.1210044. ISBN 978-0-7695-1884-8.
- ↑ «Formal Verification: An Essential Tool for Modern VLSI Design by Erik Seligman, Tom Schubert, and M V Achutha Kirankumar» (en anglès).
- ↑ «Formal Verification in Industry» (en anglès). [Consulta: 20 setembre 2012].