ENGINEERINGNET.BE - 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.
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.
In de toekomst kunnen deze ideeën ervoor zorgen dat kritieke software sneller en goedkoper ontwikkeld kan worden. 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.
