Hoewel computers tegenwoordig overal om ons heen gebruikt worden, blijkt nog steeds regelmatig dat ze erg lastig correct te programmeren zijn. Denk maar aan de storing bij ING dit voorjaar, waardoor klanten het verkeerde banksaldo te zien kregen. In het verleden hebben fouten in computersystemen geleid tot fatale problemen in raketten, vliegtuigen en medische apparatuur. Aan de UT doet men onderzoek om dergelijke problemen tot het verleden te laten behoren. “We maken gebruik van Markov-automaten, een nieuw wiskundig kansmodel dat verscheidene oude technieken verenigt. Hierdoor is het mogelijk om computersystemen steeds preciezer te modelleren en op meer en meer kwaliteitsaspecten te controleren.” Mark Timmer promoveert op dit onderwerp op vrijdag 13 september.
Sinds enkele decennia werken informatici aan het concept model checking, waarbij computersystemen gemodelleerd worden en vervolgens automatisch op fouten kunnen worden gecontroleerd. Deze techniek is een belangrijke aanvulling op het ouderwetse testen, waarbij een systeem verscheidene keren wordt uitgevoerd in de hoop dat aanwezige fouten aan het licht komen. Bij model checking, daarentegen, kunnen bepaalde problemen met wiskundige precisie worden uitgesloten.
Model checking van levensbelang
“Voor sommige toepassingen is correctheid essentieel,” vertelt Mark Timmer. “Hoewel het bij bijvoorbeeld een spelletje of een boekhoudprogramma nog geen ramp is als er enkele fouten in de software overblijven en achteraf gerepareerd moeten worden, moet je daar niet aan denken bij een raket of kerncentrale. Dan is model checking dus van levensbelang.”
Efficiënter en preciezer modelleren nu mogelijk
Traditioneel wordt bij model checking slechts gekeken naar de volgorde van gedragingen van een systeem. “Zo mag een spoorboom nooit omhoog staan op het moment dat er een trein langs komt rijden. Soms wil je echter meer, en is het ook van belang om kwantitatieve aspecten, zoals door kansen bepaald gedrag en tijdsduren, in beschouwing te nemen.” Mark Timmer werkte daarom aan het verbeteren van een uitbreiding van de technologie, die het mogelijk maakt om met dit soort kenmerken rekening te houden. “We kunnen nu op een efficiëntere wijze nog preciezer modelleren, bijvoorbeeld door aan te geven dat een bepaald onderdeel gemiddeld na 10.000 gebruiksuren defect raakt, dat een spoorwegwissel er 3 seconden over doet om naar een andere stand te schakelen of dat een bedieningssignaal met 0,1% kans niet goed aankomt. Vervolgens kunnen dan ook kwantitatieve eigenschappen berekend worden, zoals de kans dat een spoorboom minstens 1 seconde te vroeg omhoog gaat,” zegt Mark Timmer. Met de alsmaar toenemende complexiteit van computersystemen en het steeds belangrijker worden van aspecten zoals betrouwbaarheid en prestaties, is dit een belangrijke stap voorwaarts.
Promovendi voor de klas
Mark heeft tijdens zijn promotietraject als een van de eersten deelgenomen aan het project ‘promovendi voor de klas’, en hiermee de eerstegraads lesbevoegdheid behaald voor wiskunde in het middelbaar onderwijs. Sinds september 2012 is hij in deeltijd werkzaam bij het Carmel College Salland te Raalte, waar hij met veel plezier lessen verzorgt in de eerste tot en met de zesde klas. Na zijn verdediging zal hij gedeeltelijk in dienst blijven op de UT, en gedeeltelijk werkzaam blijven in het middelbaar onderwijs. Bovendien neemt hij deel aan de 'Community of Learners', een professionaliseringsproject van instituut ELAN dat docenten bij elkaar brengt om hun eigen lespraktijk te onderzoeken en te verbeteren.
Meer informatie
Op vrijdag 13 september om 16.45 uur vindt de promotie (openbaar toegankelijk) van Mark Timmer van de vakgroep Formele Methoden en Tools van het Instituut CTIT plaats in gebouw de Waaier op de campus van de UT. Zijn promotoren zijn professor Joost-Pieter Katoen en professor Jaco van de Pol, co-promotor is Mariëlle Stoelinga. Het proefschrift ‘Efficient Modelling, Generation and Analysis of Markov Automata’ is per e-mail opvraagbaar.
