Kunnen de deuren van een lift openen terwijl deze beweegt? Hoe moet de lift aangestuurd worden om zo goed en zo snel mogelijk passagiers te vervoeren? Om veilig en efficiënt te zijn moet besturingssoftware heel goed gecontroleerd worden. Dit gebeurt bijvoorbeeld met Model Checking. Anton Wijs, onderzoeker van het Centrum voor Wiskunde en Informatica (CWI) in Amsterdam, hoopt op dit onderwerp op 2 oktober 2007 aan de Vrije Universiteit te promoveren.
Model Checking is het modelleren en systematisch verifiëren van complexe softwaresystemen. Bij verificatie wordt vastgesteld of een representatief model van zo'n systeem - zoals een lift of een analysator van chemicaliën - bepaalde eigenschappen heeft of juist niet. Wijs onderzocht wat er nodig is om met Model Checking tijdkritische systemen te controleren. Er moeten dan modellen worden gemaakt waarin het systeemgedrag beschreven wordt in de tijd, zoals 'de lift doet er vijf seconden over om één verdieping omhoog te gaan' of 'de chemische reactie duurt drie seconden'. In zijn proefschrift vergelijkt Wijs verschillende modelleertalen met betrekking tot het gebruik van tijd. Verder demonstreert hij het verifiëren van enkele tijdkritische systemen.
Wijs onderzocht ook het doorzoeken van tijdgerelateerde modellen. Hij geeft een overzicht van bestaande zoekmethodes en stelt uitbreidingen voor. Eén bepaalde methode - 'beam search' - wordt door Wijs efficiënter en algemeen toepasbaar gemaakt.
Het Centrum voor Wiskunde en Informatica is sinds 1946 het nationale onderzoeksinstituut voor wiskunde en informatica. De komende jaren richt het CWI zich op vier thema's: aard- en levenswetenschappen, data-explosie, maatschappelijke logistiek en software als service.
-Meer informatie: Proefschrift: 'What to Do Next? Analysing and Optimising System Behaviour in Time'. Promotoren: prof. dr. W.J. Fokkink en prof. dr. J.C. van de Pol. Het onderzoek is uitgevoerd op het CWI, onder de auspicieën van onderzoeksschool IPA en gefinancierd door NWO.
