Minder softwarefouten door moderne kansmodellen

Het gebruik van Markov-automaten leidt tot minder softwarefouten. Dat concludeert de Twentse promovendus Mark Timmer, die werkte aan verbetering van de model-checking-aanpak met dit nieuwe wiskundige kansmodel. Op 13 september verdedigt hij aan de UT zijn proefschrift ’Efficient modelling, generation and analysis of Markov automata‘. Zijn promotoren zijn Joost-Pieter Katoen en Jaco van de Pol.

Markov-automaten maken het mogelijk om computersystemen preciezer te modelleren en op meer kwaliteitsaspecten te controleren, legt Timmer uit. ’We kunnen bijvoorbeeld aangeven dat een onderdeel gemiddeld na tienduizend gebruiksuren defect raakt, dat een spoorwegwissel er drie seconden over doet om naar een andere stand te schakelen of dat een bedieningssignaal met 0,1 procent kans niet goed aankomt. Vervolgens kunnen we dan ook kwantitatieve eigenschappen berekenen, zoals de kans dat een spoorboom minstens 1 seconde te vroeg omhooggaat.‘