A formális igazolás vagy formai igazolás annak formális igazolása, hogy az ellenőrzés tárgya megfelel-e vagy nem felel meg a formai leírásának. A téma az algoritmusok, programok és egyéb bizonyítások.
Az egyszerű formális ellenőrzések rutinszerűsége és teljes automatizálásuk elméleti lehetősége miatt a formális ellenőrzés általában automatikus, program segítségével történő ellenőrzést jelent .
A szoftvertesztelés nem tudja bizonyítani, hogy egy rendszer, algoritmus vagy program nem tartalmaz hibát és hiányosságot, és megfelel egy bizonyos tulajdonságnak. Ezt formális ellenőrzéssel lehet megtenni .
A formális ellenőrzés felhasználható olyan rendszerek ellenőrzésére, mint a forráskód szoftverek, kriptográfiai protokollok , kombinatorikus logikai áramkörök , belső memóriával rendelkező digitális áramkörök.
A verifikáció formális bizonyíték a rendszer absztrakt matematikai modelljére, feltéve, hogy a matematikai modell és a rendszer természete közötti megfelelést kezdetben adottnak tekintjük. Például modell felépítésére vagy matematikai elemzésre és algoritmusok és programok helyességének bizonyítására.
Példák a programok és rendszerek modellezésére és formális ellenőrzésére gyakran használt matematikai objektumokra:
A formális ellenőrzésnek a következő módjai vannak:
Az evidenciaalapú programozás egy olyan technológia, amelyet az 1980-as években tudományos körökben használtak olyan számítógépes programok fejlesztésére, amelyek a helyesség bizonyítékai – a programok hibáinak hiányának bizonyítékai (ez az elmélet keretein belül a hibákat az elgondolt algoritmus és az algoritmus közötti eltérésekként értelmezve). a program által megvalósított tényleges algoritmus).
A bizonyítás csak az egyszerű elméletek nagyon szűk körében automatizálható , ezért fontossá válik az automatikus verifikáció, és ehhez az igazolható formára átalakítás. A gyakorlatilag fontos problémák jelentős része, köztük például a leállási probléma , algoritmikusan megoldhatatlan .
A hitelesítő által végzett igazolások szigorúságának megőrzése érdekében ellenőrizni kell a hitelesítőt is, amelyhez még egy hitelesítő szükséges, és így tovább. Az így létrejövő hitelesítők végtelen láncolata összeomolható egy önellenőrző hitelesítő felépítésével, amely képes kibontakozni egy gyakorlatiassá.