Programverifiering

Programverifiering är processen att fastställa att ett datorprogram uppfyller en formell specifikation för samtliga tänkbara körningar. Den skiljer sig från vanlig testning genom att den i princip ger ett bevis för korrekthet i generell mening, ofta med matematiska metoder. Programverifiering används särskilt inom säkerhetskritiska och kritiska system där fel kan få allvarliga konsekvenser, eller där det krävs höga krav på felfrikhet innan distribution.

Vanliga angreppssätt inkluderar deduktiv verifiering, modellkontroll och teorembevisning. Vid deduktiv verifiering används formella bevis där programfunktioner kopplas till preconditions, postconditions och invariants. Modellkontroll och teorembevisning används på olika nivåer, från algoritmer till systemmodeller. Formella specifikationer uttrycks ofta med logiker som temporal logik (LTL eller CTL) eller med kontraktbaserade språk. Verktyg som SMT-solverar (till exempel Z3 eller CVC4), och teoremassistenter (Coq, Isabelle) stöder bevisarbete, medan modellkontrollverktyg (SPIN, NuSMV) utför systematisk utforskning av beräkningsmodeller.

Processen innebär vanligtvis att skriva en formell specifikation, skapa en modell av programmet eller dess kärnkomponenter och visa att modellen uppfyller önskade egenskaper. Praktiskt används ofta en kombination av manuell bevisning och automatiska verktyg: man gör en lämplig abstraktion, formulerar invariants och pre-/postvillkor, och använder verifieringsverktyg för att visa att egenskaperna hålls under alla tänkbara körningar. Målet kan vara fullständiga korrekthetsbevis eller verifiering av en verifierbar implementation, exempelvis av en kritisk komponent eller en certifierad kompilator.

Användningsområden inkluderar flyg- och bilindustrin, medicinsk utrustning, kryptering och andra säkerhetskänsliga system där formell verifiering bidrar till ökad tillförlitlighet. Begränsningar inkluderar skalbarhet, komplexitet hos program och kostnader för att skapa formella modeller och bevis. Framtiden ser ökade integrationer mellan verifiering och traditionell mjukvaruutveckling samt bredare användning av certifierade verktyg i kritiska programvarustackar.