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. Som Wallenberg Academy Fellow vill Niki Vazou 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 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.

Pålitliga system som är lättare att underhålla

Porträtt av Niki VazouI sin forskning strävar Niki Vazou, idag verksam vid IMDEA Software Institute i Spanien, efter att göra koncept för programverifiering konventionella, och integrera dem med funktionell programmering. På så sätt kommer framtidens programvaruutveckling att bli enklare, samtidigt som systemen blir mer pålitliga och lättare att underhålla.
– Effekten kommer att synas inom alla områden som är beroende av programvara, från sociala nätverk till banktransaktioner och utveckling av medicinsk utrustning, säger Niki Vazou.

Den nya metoden för formell verifiering ska bli en integrerad del av programvaran och samtidigt generera ett matematiskt bevis vid ett korrekt test. Om Niki Vazou accepterar utnämningen till Wallenberg Academy Fellow kommer forskningen att bedrivas vid Institutionen för data- och informationsteknik.
– Mitt intresse för funktionell programmering kommer ur en enorm kärlek till matematik, och upptäckten att matematiska funktioner kan bli interaktiva genom programspråk som till exempel Prolog och Haskell. Chalmers är det bästa europeiska universitetet inom områdena funktionell programmering och typteori, och eftersom min forskning ligger precis i skärningspunkten mellan dessa två områden ger utnämningen till Wallenberg Academy Fellow en unik möjlighet att direkt samarbeta med toppforskare inom mitt område, säger hon.

Fyra Wallenberg Academy Fellows till Chalmers 2021

Forskningsfinansieringen från Wallenberg Academy Fellowship uppgår till mellan 5 och 15 miljoner kronor per forskare under fem år beroende på ämnesområde. Efter den första periodens slut har forskarna möjlighet att söka ytterligare fem års finansiering. Här kan du läsa om de andra utnämningarna:


Sidansvarig Publicerad: to 02 dec 2021.