Formell verifiering eller formellt bevis är ett formellt bevis på överensstämmelse eller bristande efterlevnad av föremålet för verifiering med dess formella beskrivning. Ämnet är algoritmer, program och andra bevis.
På grund av den rutinmässiga karaktären hos även enkel formell verifiering och den teoretiska möjligheten till fullständig automatisering, innebär formell verifiering vanligtvis automatisk verifiering med hjälp av ett program .
Programvarutestning kan inte bevisa att ett system, en algoritm eller ett program inte innehåller några fel och defekter och uppfyller en viss egenskap. Detta kan göras genom formell verifiering.
Formell verifiering kan användas för att verifiera system som källkodsprogramvara, kryptografiska protokoll , kombinatoriska logiska kretsar , digitala kretsar med internminne.
Verifiering är ett formellt bevis på en abstrakt matematisk modell av systemet, under antagandet att överensstämmelsen mellan den matematiska modellen och systemets karaktär anses vara initialt given. Till exempel att bygga en modell eller matematisk analys och bevis på riktigheten av algoritmer och program.
Exempel på matematiska objekt som ofta används för modellering och formell verifiering av program och system är:
Det finns följande metoder för formell verifiering:
Evidensbaserad programmering är en teknik som användes i akademiska kretsar på 1980-talet för att utveckla program för datorer med korrekthetsbevis - bevis på frånvaron av fel i program (förstå, inom ramen för denna teori, fel som avvikelser mellan den tänkta algoritmen och den faktiska algoritmen som implementeras av programmet).
Beviset kan endast automatiseras helt för en mycket liten krets av enkla teorier, så dess automatiska verifiering och, för detta, omvandling till en verifierbar form blir viktig. Ett betydande antal praktiskt viktiga problem, inklusive till exempel stoppproblemet , är algoritmiskt olösliga .
För att upprätthålla rigoriteten vid kontroll av ett bevis av en verifierare bör man också kontrollera verifieraren, för vilken ytterligare en verifierare behövs, och så vidare. Den resulterande oändliga kedjan av verifierare skulle kunna kollapsas genom att bygga en självverifierande verifierare som har förmågan att utvecklas till en praktisk.