Computers en software zijn belangrijker dan ooit. Voor systemen zoals auto’s, vliegtuigen en medische apparatuur is het van cruciaal belang dat software geen grote problemen of bugs bevat. Thomas Neele, promovendus aan de Technische Universiteit Eindhoven, heeft drie technieken ontwikkeld om software slimmer en sneller te checken op bugs, gebaseerd op de model checking methode. Hij verdedigde vandaag zijn dissertatie.
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, en alle ‘toestanden’ waar het zich in kan bevinden, om te zien of alles werkt zoals het moet. 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.
Tim Willemse
Het doel van de software in gedachten houden
De methodes van Neele hebben een 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 om 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.
Jan Friso Groote
Software sneller veiliger maken
In de toekomst kunnen deze ideeën ervoor zorgen dat kritieke software sneller en goedkoper ontwikkeld kan worden. Hierdoor wordt high-tech gezondheidszorg betaalbaarder en toegankelijker. Verder kunnen Neeles technieken helpen om gevaarlijke bugs 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.
Titel van de dissertatie: Reductions for Parity Games and Model Checking. Supervisors: Tim Willemse en Jan Friso Groote, Technische Universiteit Eindhoven. Andere betrokken partijen: ASML. Bron TUE
