Can elevator doors slide open when the elevator moves? How should it be controlled to transport people as fast and as good as possible? In order to be safe and efficient the control software must be checked carefully. This can be done with Model Checking. Anton Wijs, researcher at the Centrum voor Wiskunde en Informatica (CWI) in Amsterdam, will receive his PhD on this subject on 2 October at the Vrije Universiteit Amsterdam. His thesis is titled What to Do Next? Analysing and Optimising System Behaviour in Time.
Model Checking means modelling and systematically verifying complex software systems. Verification ascertains whether a representative model- like an elevator, or, for instance, an analyser of chemicals - possesses the proper characteristics or not.
Wijs investigated what it takes to check time-critical systems with Model Checking. This implies making models in which system behaviour is described in time units, such as 'it takes the elevator five seconds to get to the next floor' or 'the chemical reaction lasts three seconds'. In his thesis Wijs compares several modelling languages in their relation to the use of time. He also demonstrates the verification of some time-critical systems.
Another aspect is searching through time-related models. Wijs gives a survey of existing search methods and proposes extensions. Next he focuses on one particular method - beam search - and makes this more efficient and generally applicable.
The PhD ceremony starts at 15.45h in the Aula of the Vrije Universiteit, De Boelelaan 1105, Amsterdam. Promotores: Prof. dr. W.J. Fokkink and Prof. dr. J.C. van de Pol.
