Hur vet vi att datorsystemet gör rätt?
Datorer finns överallt. Överallt! Och varje dator kör mängder av olika datorprogram, även kallat mjukvara, som påverkar vår vardag nästan hela tiden. I våra mobiltelefoner, i våra bilar, ja till och med våra i våra brödrostar finns det datorer. Vissa av datorprogrammen är otroligt komplicerade, medan andra ska egentligen bara göra en enda enkel sak. Men hur vet vi att alla dessa ting gör det som de ska göra? Hur vet vi att ett program inte innehåller massa buggar? Traditionell har man använt sig av testning för att säkra sig om att programmen är bugfria. Genom att provköra dem i många olika situationen och se att de inte kraschar kan man känna sig trygg att det fungerar som man ska. Eller kan man det?
I min presentation visar jag begränsningen av mjukvarutestning och berättar om ett alternativt sätt att säkerställa funktionaliteten hos ett program. Med formella metoder, en slags logisk analys, kan vi bevisa att ett program är korrekt och få en hundra-procentig garanti för att ett det följer sin funktionalitet.
På Mälardalens Universitet i Västerås så forskar jag på hur man tillämpa så kallad formell verifiering, d.v.s. en matematisk analys, på olika typer av system för att kunna bevisa att system gör det som de ska i kritiska situationer. Detta blir desto mer viktigt ju fler aspekter av våra liv som är beroende av att datorsystem inte felar.
Kontakt:
Peter Backeman
Postdoktor vid akademin för innovation, design och teknik (IDT) vid Mälardalens universitet
