Verificació del programari

La verificació de programari és una disciplina d'enginyeria de programari, llenguatges de programació i teoria de la computació l'objectiu de la qual és assegurar que el programari compleixi els requisits esperats.^[1]

Una definició àmplia de verificació fa que estigui relacionada amb les proves de programari. En aquest cas, hi ha dos enfocaments fonamentals per a la verificació:

• Verificació dinàmica, també coneguda com a experimentació, prova dinàmica o, simplement, prova. - Això és bo per trobar errors (errors de programari).
• Verificació estàtica, també coneguda com a anàlisi o, prova estàtica: és útil per demostrar la correcció d'un programa. Tot i que pot donar lloc a falsos positius quan hi ha un o més conflictes entre el procés que realment fa un programari i el que la verificació estàtica suposa que fa.^[2]

Sota l'ACM Computing Classification System, els temes de verificació de programari apareixen a "Programari i la seva enginyeria", a "Creació de programari", mentre que la verificació de programes també apareix a Teoria de la computació a Semàntica i raonament, Raonament de programes.

La verificació dinàmica es realitza durant l'execució del programari i en comprova dinàmicament el comportament; es coneix comunament com la fase de prova. La verificació és un procés de revisió. Segons l'abast de les proves, les podem classificar en tres famílies:

• Prova en petit : una prova que verifica una funció o classe única (prova unitaria)
• Prova en gran : una prova que verifica un grup de classes, com ara
  • Test de mòdul (un sol mòdul)
  • Prova d'integració (més d'un mòdul)
  • Prova del sistema (tot el sistema)
• Prova d'acceptació : una prova formal definida per comprovar els criteris d'acceptació d'un programari
  • Prova funcional
  • Prova no funcional (rendiment, prova d'esforç)

L'objectiu de la verificació dinàmica de programari és trobar els errors introduïts per una activitat (per exemple, disposar d'un programari mèdic per analitzar dades bioquímiques); o per la realització repetitiva d'una o més activitats (com ara una prova d'esforç per a un servidor web, és a dir, comprovar si el producte actual de l'activitat és tan correcte com ho era al començament de l'activitat).^[3]

La verificació estàtica és el procés per comprovar que el programari compleix els requisits mitjançant la inspecció del codi abans que s'executi. Per exemple:

• Verificació de les convencions del codi
• Detecció de males pràctiques (anti-patró).
• Càlcul de mètriques de programari
• Verificació formal

Verificació per anàlisi: el mètode de verificació d'anàlisi s'aplica a la verificació per investigació, càlculs matemàtics, avaluació lògica i càlculs que utilitzen mètodes clàssics de llibres de text o mètodes informàtics d'ús general acceptats. L'anàlisi inclou el mostreig i la correlació de les dades mesurades i els resultats de les proves observades amb els valors esperats calculats per establir la conformitat amb els requisits.^[4]

Quan es defineix de manera més estricta, la verificació és equivalent només a les proves estàtiques i està pensada per aplicar-se als artefactes. I, la validació (de tot el producte de programari) seria equivalent a les proves dinàmiques i es pretén aplicar al producte de programari en execució (no els seus artefactes, excepte els requisits). Tingueu en compte que la validació de requisits es pot realitzar de manera estàtica i dinàmica (vegeu la validació d'artefactes).^[5]

La verificació de programari sovint es confon amb la validació de programari. Diferència entre verificació i validació:

• La verificació del programari fa la pregunta: "Estem construint bé el producte?"; és a dir, el programari s'ajusta a les seves especificacions? (A mesura que una casa s'ajusta als seus plànols.)
• La validació del programari fa la pregunta: "Estem construint el producte adequat?"; és a dir, el programari fa el que realment requereix l'usuari? (Com una casa s'ajusta al que el propietari necessita i vol.)