Formel verifikation eller formel bevis er et formelt bevis for, at verifikationsobjektet overholder eller ikke overholder dets formelle beskrivelse. Emnet er algoritmer, programmer og andre beviser.
På grund af den rutinemæssige karakter af selv simpel formel verifikation og den teoretiske mulighed for deres fuldstændige automatisering, betyder formel verifikation normalt automatisk verifikation ved hjælp af et program .
Softwaretest kan ikke bevise, at et system, en algoritme eller et program ikke indeholder fejl og mangler og opfylder en bestemt egenskab. Dette kan gøres ved formel verifikation.
Formel verifikation kan bruges til at verificere systemer såsom kildekodesoftware, kryptografiske protokoller , kombinatoriske logiske kredsløb , digitale kredsløb med intern hukommelse.
Verifikation er et formelt bevis på en abstrakt matematisk model af systemet, under den antagelse, at overensstemmelsen mellem den matematiske model og systemets karakter anses for at være givet. For eksempel at bygge en model eller matematisk analyse og bevis for rigtigheden af algoritmer og programmer.
Eksempler på matematiske objekter, der ofte bruges til modellering og formel verifikation af programmer og systemer, er:
Der er følgende tilgange til formel verifikation:
Evidensbaseret programmering er en teknologi, der blev brugt i akademiske kredse i 1980'erne til at udvikle programmer til computere med beviser for korrekthed - beviser for fravær af fejl i programmer (forståelse inden for rammerne af denne teori, fejl som uoverensstemmelser mellem den udtænkte algoritme og den faktiske algoritme implementeret af programmet).
Beviset kan kun automatiseres fuldt ud for en meget lille kreds af simple teorier, så dets automatiske verifikation og, for dette, transformation til en verificerbar form bliver vigtig. Et betydeligt antal praktisk vigtige problemer, herunder for eksempel stopproblemet , er algoritmisk uløselige .
For at opretholde stringens, når en verifikator kontrollerer et bevis, bør man også kontrollere verifikatoren, for hvilken der er behov for en verifikator mere, og så videre. Den resulterende uendelige kæde af verifikatorer kunne brydes sammen ved at bygge en selvverificerende verifikator, der har evnen til at udfolde sig til en praktisk.