FEWER SOFTWARE ERRORS BY USING MODERN STOCHASTIC MODELS
Although everywhere we look we see computers being used, it seems that programming them correctly is still a tricky problem. Just look at what happened during the ING breakdown in the spring of this year, which resulted in clients seeing the wrong bank balance. Past errors in computer systems have been the cause of fatal problems with rockets, aeroplanes and medical apparatus. Research is being done at the UT that will make such problems a thing of the past. “We are using Markov automata, a new mathematical probability model that combines various old techniques. This makes it possible to model computer systems with increasing precision and to monitor a growing number of quality aspects.” Mark Timmer will obtain his doctorate with a thesis on this subject on Friday 13 September.
For some decades information experts have been working on the concept of model checking, which permits the modelling of computer systems so they can subsequently be automatically monitored for errors. This technique is an important addition to old-fashioned tests that involve implementing a system several times in the hope that any errors present will come to light. Model checking, however, allows us to preclude certain problems with mathematical precision.
Model checking vitally important
“Correctness is essential for some applications,” says Mark Timmer. “For example, though it may not be a disaster if there are still a few errors in software for a game or a bookkeeping programme and retrospective repairs will be needed, this is something that cannot even be contemplated in relation to a rocket or an atomic power station. This is what makes model checking of such vital importance.”
More efficient and accurate modelling is now possible
Traditionally, model checking only examined the sequence of a system's behaviours. “For example, a level-crossing barrier may never be open at the moment at which a train is passing. But sometimes you want more, and it is also important to consider quantitative aspects as well, such as behaviour that is subject to probability and the times involved.” This is what brought Mark Timmer to work on improving an expansion in technology that has made it possible to take such characteristics into account. “We are now able to apply models with even greater precision, for example, by indicating that, on average, a given part will become defective after 10,000 hours of use, that a rail-road switch takes 3 seconds to switch to a different position or that the probability of a control signal being processed incorrectly is 0.1%. We can then go on to calculate quantitative properties, such as the chance that a level-crossing barrier will open 1 second too early,” says Mark Timmer. This represents an important step forwards, in view of the steadily increasing complexity of computer systems and the increasing importance of such aspects as reliability and performance.
Ph D students giving lessons
Druing the course of his doctoral study, Mark was one of the first to participate in the project ‘lessons from Pd D students’, as a result of which he has achieved full qualifications for teaching mathematics in secondary education. Since September 2012 he has been working part-time at the Carmel College Salland in Raalte, where he is enjoying giving lessons to pupils in classes ranging from the first to the final year. After defending his thesis he will remain parlty in the service of the UT, while continuing to work part-time in secondary education. In addition, he will participate in the 'Community of Learners', a professionalization project set up by the ELAN institute, which brings teachers together in order to examine and improve their methods of teaching.
More information
The thesis defence ceremony of Mark Timmer, of the Methods and Tools Department of the CTIT Institute, will take place on Friday 13 September at 16.45 hours in the 'De Waaier' building on the UT campus. His supervisors are Professor Joost-Pieter Katoen and Professor Jaco van de Pol, and his co-supervisor is Mariëlle Stoelinga. The thesis, ‘Efficient Modelling, Generation and Analysis of Markov Automata’ can be requested by e-mail.
