A szoftverbiztonság a mostanában kialakuló információs társadalom kulcsfontosságú eleme. A kibernetikai rendszerek különböző problémái a szoftverrendszerek helytelen viselkedésére vezethetők vissza, amit elsősorban a szoftveralapú rendszerek nagyfokú bonyolultsága okoz, valamint ezek ellenőrzésére szolgáló gyakorlati módszerek hiánya.
Egy olyan gyakorlati szoftvertanúsítási módszertant javaslunk, amely kombinálja a szoftver formális verifikációját, és a szoftver helyességét igazoló konkrét dokumentumok előállítását. A módszertan több szoftvercégtől kapott valós körülményeket tartalmazó esettanulmányon keresztül szemléltetjük, amely során felhasználjuk az jelenleg elérhető szoftverfejlesztési, program helyesség ellenőrző és automatikus tételbizonyító eszközöket.
A javasolt módszertan a következőket foglalja magában: formális modellezés, formális specifikáció, elő- és utófeltételek használata, helyesség bizonyítása és fokozatos finomítás. Először a szoftver komponenshez szükséges folyamat formális modelljét kell kifejleszteni. Először a szoftver komponenshez szükséges folyamat formális modelljét kell kifejleszteni. Ez magában foglalja a matematikai elméletet, amely tartalmazza a megvalósítandó funkciők szempontjából releváns fogalmakat és tulajdonságokat, ezek logikai leírását, vagyis ezek formális specifikációját. Ez alapján a funkciókat megvalósító algoritmusok logikai szinten vannak kifejlesztve (függetlenül az adott rendszerkörnyezettől vagy programozási nyelvtől). Az elő- és utófeltételeket automatikusan generáljuk a formális specifikációból és az algoritmusok logikai leírásából. Végül az elő- és utófeltételeket automatizált érvelés segítségével bizonyítjuk, amely felhasználja modellhez rendelt elméletet (definíciókat és tételeket) és azokat a specifikus következtetési lépéseket, amelyek a tárgykör objektumaihoz kapcsolódnak. A módszerünk megkülönböztető jellemzője az intuitív bizonyítások előállítása, amelyek az emberek által olvashatóak, így a tanúsítás megalapozottságát erősítik. A rendszer bonyolultságától függően a fenti műveletek sorát kell ismételni az absztrakció különböző szintjei, illetve különálló funkcionális blokkokra úgy, hogy az egyes rész-tevékenységek komplexitását a probléma felbontásával csökkentjük.
