Met modelchecken worden ICT-systemen niet gegarandeerd foutvrij, maar ze leiden wel tot een veel grotere betrouwbaarheid, aldus Arend Rensink, hoogleraar Software Modelling, Transformation and Verification en begeleider van het promotieonderzoek.

Reguliere testen zijn nooit afdoende om alle mogelijke foutcombinaties vooraf te voorzien. Het aantal scenario's is namelijk oneindig groot. En dus kan er, ook na uitgebreid testen, nog van alles misgaan. “Op dit moment worden in de IT vooral vooraf bedachte scenario's getest, maar als je er een vergeet, kan het zijn dat de software bij alsnog vastloopt", vertelt Rensink tegen Webwereld. “Bij modelchecken kijk je veel meer naar de specificaties van een systeem en naar wat zo'n systeem behoort te doen. In de praktijk blijkt het checken van die specificaties op basis van modellen veel betrouwbaarder te zijn."

Modelchecken

Modelchecken (bijvoorbeeld met de modelleertool GROOVE) is een geavanceerde wiskundige manier van computersystemen checken, die bij de Universiteit van Twente vooral grafisch wordt opgelost. Andere onderzoeksgroepen in de wereld richten zich meer op tekstuele modellen. “Grafische modellen zijn visueel ook beter te begrijpen", stelt Rensink.

Op de Universiteit Twente doet men al tien jaar onderzoek naar modelchecken. De modellen worden onder meer gebruikt voor het testen van data bij de NS voor de werking van spoorwegwissels. In de praktijk zouden seinstoringen daardoor beter verholpen kunnen worden. “Het is waar dat je ook in dat geval niet alle problemen kunt voorspellen, zeker als er externe factoren een rol spelen, denk aan weersomstandigheden, maar de programmacode zelf wordt er wel schoner door", zegt Rensink.

Niet meer eindeloos testen

Modelchecken leent zich echter niet alleen voor bedrijfskritische toepassingen, benadrukt Rensink: “Je ziet een trend bij niet-bedrijfskritische toepassingen dat men vanwege de kosten software niet meer eindeloos test, en fouten gaandeweg herstelt. Opdrachtgevers en gebruikers nemen daar ook steeds vaker genoegen mee. Met modelchecken kun je een veel beter resultaat bereiken gelijk al in het begin. De testperiode kun je met tientallen procenten terugbrengen."

Rensink hoopt de technologie onder de aandacht te brengen bij het bedrijfsleven. De potentie van modelchecken is volgens hem nog niet echt ontdekt.

Betrekking in Brazilië

De Braziliaanse UT-promovendus Eduardo Zambon van het CTIT Instituut voor Telematica en Informatietechnologie zal een eventueel vervolgtraject echter niet meer meemaken. Hij heeft een goede betrekking kunnen krijgen in zijn thuisland. “Hij heeft de bestaande techniek geschikt gemaakt voor grotere systemen, het is jammer dat hij vertrekt."