Overview of formal methods in software engineering

Det vanligaste sättet att leta efter fel och buggar i IT-system är att använda testning, simulering och manuell kodgranskning. Dessa tekniker är dock inte uttömmande och kan inte garantera frånvaro av defekter. En mer lovande metod är att använda formella metoder under IT-systemets utvecklingsprocess, till exempel genom att skriva en formell specifikation för systemet genom vilken olika egenskaper kan bevisas och sedan matematiskt bevisa att implementationen följer specifikationen. I denna rapport avser vi att ge en kortfattat introduktion till forskningen kring formella metoder tillsammans med en klassificering av de olika existerande formella metoderna. Vi guidar också läsaren genom ett urval av forskningslittarturen inom området och vi presenterar några system där formella metoder använts för att bevisa säkerhetsegenskaper. Även en överblick av ett funktionellt riktighetsbevis för en säkerhetskritisk mikrokärna ges. Utifrån den litteraturstudie vi gjort kan vi konstatera att användning av formella metoder verkar vara kostnadseffektivt i det långa loppet och att det reducerar antalet defekter till nära noll. Oavsett det har metoderna ännu inte fått någon större spridning och det finns därför ett begränsat antal verktyg att tillgå.