Matematiskt spel gör datorn säker
Att bordsdatorn kraschar kan vara nog så besvärligt, men om det drabbar de datorer som reglerar trafikljus eller flygplansroder blir konsekvenserna betydligt värre. Sven Sandberg har utvecklat metoder för att hitta vinnande strategier i spel, med vilkas hjälp det är möjligt att konstruera säkra programsystem. Han försvarar sin avhandling vid Uppsala universitet den 23 mars.
Vid kontroll av säkerhetskritiska datorsystem räcker det inte med vanlig systematisk testning, istället behövs en ännu säkrare metod. Ofta använder man sig av modellkontroll, vilket innebär att man skapar en matematisk modell som är en förenklad bild av systemet. Därefter låter man en dator undersöka modellen för att bevisa att den är korrekt.
De flesta modeller av system innehåller tillstånd och övergångar, där tillstånden utgörs av tänkbara situationer och övergångarna anger på vilket sätt situationerna kan följa varandra. En modell för ett system som styr ett trafikljus kan till exempel använda de tre tillstånden rött, gult och grönt, samt övergångarna mellan dessa. Ett viktigt verktyg för att verifiera sådana modeller av system är spelteori.
– Man kan se det som ett spel, där det gäller att reglera flera par trafikljus i en korsning så att trafikanterna aldrig krockar. Ifall man lyckas hitta en vinnande strategi kan den användas för att skapa ett system som bevisbart är helt säkert, förklarar Sven Sandberg, som har arbetat med att utveckla metoder för hur man hittar den bästa strategin i ett givet spel.
I avhandlingen har han undersökt två olika kategorier av modeller – spelmodeller och slumpmässiga modeller, där antalet tänkbara tillstånd är oändligt. Slutligen förenar han dessa områden och studerar spel som innehåller dels slumpmässiga moment, dels oändligt många tillstånd.
– Just de här modellerna kan användas för att beskriva datorer eller andra maskiner som kommunicerar på avstånd. Vi vill fastställa att ingen illasinnad utomstående kan få vår maskin ur balans genom att skicka felaktiga meddelanden till den, och det gör vi genom att undersöka ett spel mellan vår egen maskin och en tänkt ”motståndare”. Ifall det finns något sätt för maskinen att vinna över motståndaren kan den vinnande strategin användas för att skapa en beskrivning av hur maskinen ska fungera, berättar han.
Kontaktinformation
För mer information, kontakta Sven Sandberg, 018-471 10 49, e-post: svens@it.uu.se
