Verificació formal

La verificació formal, en ingenieria i en computació, és un método de validació estàtica (es valida a través del propi còdic del programa, a partir d'una abstracció o d'una representació simbòlica) en el que, partint d'un conjunt axiomàtic, regles d'inferència i algun llenguage llògic (com la llògica de primer orde), es pot trobar una demostració o prova de correcció d'un programa, algoritme, etc, encara que també es pot trobar la seua refutació. És un método necessari per a provar qualsevol programa o teoria pero, encara que siga satisfactòria, no assegura que la solució siga del tot correcta.

Dins de la computació, la verificació és usada per a estudiar els distints sistemes software (en còdic font), sistemes combinacionales, circuits digitals, etc.

Un dels precursors de la verificació va ser Edsger Dijkstra que, mostrant molt interés en ella durant els 70, va publicar el llibre "A Discipline of Programming", en el qual, va presentar el seu método de desenroll sistemàtic de programes junt en les seues proves de correcció, tots ells basats en la verificació formal.

Verificació Formal

Archiu:ModelChecking es.svg

Els métodos de verificació formal solen permetre verificar automàticament si un sistema satisfà una propietat donada. A diferència de les proves o la simulació, la verificació formal considera tots els comportaments possibles del sistema. Existixen tres métodos bàsics de verificació formal:

• Comprovació d'equivalència: determina si un sistema és equivalent a la seua especificació sobre un tipo donat d'equivalència de comportament.

• Comprovació de models: determina si un sistema satisfà una propietat donada. Si el sistema no la satisfà, la comprovació de models pot mostrar un contraeixemple, és dir, un comportament del sistema que la viola.

• Demostració de teoremes: el sistema i les seues propietats s'expressen com una fòrmula en un dels sistemes de llògica matemàtica, i la demostració de teoremes busca la demostració de la propietat. Este procés encara no és completament automàtic.

Les propietats que es deuen verificar es descriuen a sovint en llògiques temporals, com la llògica temporal llineal (LTL) o la llògica d'arbre computacional (CTL).

Alguns programes en llenguages funcionals poden verificar-se formalment per mig de equivalència i induccions. A voltes, es pot demostrar que el còdic del llenguage imperatiu és correcte, o és correcte, utilisant la llògica de Hoare.

Importància en les matemàtiques

Tradicionalment, dins de les matemàtiques, la verificació únicament s'utilisava per a la demostració i convicció d'enunciats matemàtics i com a mig d'obtenció d'evidències per a l'eliminació de dubtes. Pero en la realitat té un major número de funcions, aparte de la de convicció:

• En el seu us típic de convicció, com s'ha dit anteriorment, es basa en la demostració d'enunciats i de conjectura desconegudes, verificació deductiva. En este estudi, els matemàtics, ademés de partir de les premisses, construïxen contraeixemples per mig d'una série de proves, cridades proves cuasi-empíriques, les quals, intenten descobrir contradiccions o errors amagats.

Un dels métodos d'esta verificació, és la cridada demostració deductiva, en a on la conclusió prové de les premisses. Un defecte d'esta demostració, és que es dona lloc uns desenrolls tan extensos i complicats que el risc de cometre errors aumenta.

Com a método de sistematisació. Ací, la verificació no comprova si algunes afirmacions són certes o no, sino que s'encarrega d'organisar enunciats individuals no relacionats. D'esta manera, ajuda a identificar inconsistencias, a simplificar les teories matemàtiques (integrant afirmacions i teoremes), a economizar els resultats, a ajudar a les aplicacions per mig de l'anàlisis dels seus axioma i definicions, etc.

Com a método d'explicació. Encara que és possible alcançar l'afirmació per mig de la verificació deductiva, en la majoria dels casos, esta no proporciona una explicació vàlida de per qué pot ser verdader i únicament confirma que és veritat. Aixina, en els casos en els que els resultats estan defesos per evidències cuasi-empíriques concloents, la funció de la verificació no és únicament la de convéncer, sino també la d'explicar. Més encara, per als matemàtics és més primordial este aspecte aclaratorio, que el simple fet de verificació.

• Com a verificació de models. Este tipo de verificació, consistix en un reconeiximent del model matemàtic (aplicable tant para models finitos, com per a models infinits, ya que estos últims es poden representar de manera finita per mig de l'abstracció).

En definitiva, consistix en estudiar tots els canvis i estats dels models matemàtics per mig de tècniques inteligents d'abstracció, conseguint agrupar en una sola operació tot el conjunt d'estats. Estes transicions estudiades, són descrites en diferents llògiques, tals com, la llògica computacional, la llògica temporal ...

Vore també

• Llògica de Hoare, un sistema formal que permet la verificació de programes imperatius.
• Llenguages formals.
• Método formal.
• Verificació de models.

Bibliografia

• Edsger Dijkstra, Wim H. J. Feijen, A Method of Programming, Addison-Wesley, 1988, 188 pages
• Gila Hanna, Més que demostració formal, 1989