Controle van software op bugs ondergaat verbetering

Software is in de toekomst slimmer te checken op bugs. Nieuwe ideeën zorgen ervoor dat kritieke software straks sneller en goedkoper is te ontwikkelen. Met name voor systemen zoals auto's, vliegtuigen en medische apparatuur is het van cruciaal belang dat software geen grote problemen of 'bugs' bevat.

Thomas Neele promoveert woensdag aan de Technische Universiteit Eindhoven op het beter controleren van software op bugs. De computerwetenschapper heeft daartoe drie technieken ontwikkeld gebaseerd op de zogenoemde ‘model checking’-methode.  Hij ontwierp daartoe een aantal algoritmes.

Model checking is een van de meest rigoureuze technieken om software te checken. Er wordt gekeken naar alle mogelijke acties die een softwaresysteem kan doen. Om te zien of alles werkt zoals het moet, worden ook alle ’toestanden’ onderzocht waar het systeem zich in kan bevinden.

De uitdaging is dat software vaak uit meerdere delen bestaat die naast elkaar hun werk doen. Daardoor kan het aantal toestanden om te checken explosief toenemen, wat model checking duur en soms zelfs ondoenbaar maakt. Neele heeft nieuwe manieren verkend om dit probleem aan te pakken en ervoor te zorgen dat minder toestanden gecheckt hoeven te worden.

Gedrag

Zijn methodes hebben één ding gemeen: ze houden per toestand de vereisten in de gaten. Deze extra informatie maakt het makkelijker om te bekijken welke toestanden niet gecheckt hoeven te worden. Om tegelijkertijd naar het systeemgedrag en de vereisten te kunnen krijgen, moest Neele eerst een nieuwe, gestructureerde manier ontwikkelen om de combinatie van vereisten en gedrag te laten zien.

De eerste techniek vermindert het aantal toestanden om te checken door gelijksoortige toestanden bij elkaar te groeperen. Dit maakt het zelfs mogelijk met een oneindig aantal toestanden te werken. De tweede methode controleert of parallelle onderdelen soms onafhankelijk van elkaar werken. Als dat zo is, dan is het niet nodig om alle mogelijke toestanden te bestuderen. De laatste techniek controleert of bepaalde informatie relevant is en verwijdert die als dat niet zo is.

Gevaarlijke bugs

In de toekomst kunnen deze ideeën zorgen voor een versnelde ontwikkeling van kritieke software.  Hierdoor wordt vooral de hi-techgezondheidszorg betaalbaarder en toegankelijker. Verder kunnen Neeles technieken helpen om in bijvoorbeeld vliegtuigen te voorkomen. Op dit moment is er veel expertise nodig om Neeles ideeën, en model checking in het algemeen, te kunnen toepassen. Om meer algemeen gebruik mogelijk te maken, moet er een volledig geautomatiseerd systeem gebouwd worden dat bepaalt welke methode het beste past bij specifieke toepassingen.

De titel van de dissertatie luidt ‘Reductions for Parity Games and Model Checking’. Supervisors zijn prof. Tim Willemse en prof. Jan Friso Groote, beiden van de Technische Universiteit Eindhoven. ASML is bij het project betrokken.