Ny metod för att verifiera programvaror

När utvecklare ska säkerställa att en programvara fungerar korrekt, kan de i dag välja mellan två metoder. Den ena är opraktiskt att använda, men rigorös. Den andra är lättare att använda, men mindre tillförlitlig. Wallenberg Academy Fellow Niki Vazou ska nu utveckla en metod som både är lättanvänd, och vilar på en rigorös grund. 

När program för till exempel banktransaktioner, smarta bilar eller sjukhusutrustning, implementeras måste de fungera korrekt. För att säkerställa detta använder utvecklare något som kallas för formell verifiering. Det kan exempelvis handla om att testa att ingen privat information läcker ut från systemet, eller att krypteringen fungerar som den ska. 

I dagsläget finns två metoder för formell verifiering. Inom den traditionella formen använder man sig av en gren inom matematiken som kallas för typteori. Om programkoden fungerar, kommer verifieringen att generera ett matematiskt bevis för detta. Metoden är därför rigorös, men av olika skäl är den opraktisk att använda. 

Många jobbar i stället med en annan metod, typsystem för förfining, som kan utvecklas i ett vanligt programmeringsspråk. Det är en praktisk form av verifiering som kan bli en integrerad del av programvaran. Men detta system vilar inte på samma starka matematiska grund.

Dr Niki Vazou vid IMDEA Software Institute, Spanien, ska nu utveckla en metod för formell verifiering, som både kan bli en integrerad del av programvaran och samtidigt genererar ett matematiskt bevis vid ett korrekt test. 

Som Wallenberg Academy Fellow kommer hon att vara verksam vid Chalmers tekniska högskola. 

Foto: Niki Vazou