Stel je eens voor dat we nooit meer computerproblemen hebben. Geen gedoe bij seinstoringen op het spoor, geen ongelukken meer, altijd veilig internetbankieren of alle medische apparatuur op orde. Dat zou een droomwereld zijn. Want bij computersystemen horen nu eenmaal fouten en we kunnen toch wel een keertje iets over het hoofd zien? Nou niet dus. We hoeven niets meer over het hoofd te zien volgens UT-promovendus Eduardo Zambon van het CTIT Instituut voor Telematica en Informatietechnologie. Want met modelchecken halen we de fouten uit de systemen en dan zijn de systemen dus gegarandeerd foutvrij. De Braziliaan Zambon promoveert op dit onderwerp op donderdag 24 januari 2013.
Modelchecken is iets anders dan het testen van computersystemen. Bij testen kunnen wel fouten getraceerd worden in de systemen, maar het is nooit afdoende om alle mogelijke foutcombinaties vooraf te voorzien. Met modelchecken (bijvoorbeeld door de inzet van de modelleertool GROOVE), een geavanceerde wiskundige manier van computersystemen checken, lukt dat wel. Op de Universiteit Twente doet men daar sinds tien jaar onderzoek naar. “We willen de wereld graag vertellen, dat we hier heel ver mee zijn en dat het bedrijfsleven, maar ook de overheid op termijn kan profiteren van ons onderzoek”, vertelt Arend Rensink (Professor Software Modelling, Transformation and Verification) en promotor (begeleider) van Eduardo Zambon. “We helpen de programmeur op weg, zodat hij straks de betrouwbaarheid van zijn software kan garanderen.”
“Je moet je voorstellen dat er bij computersystemen oneindig veel geanalyseerd kan worden, het aantal mogelijk scenario’s is niet te overzien. Er kan van alles misgaan op manieren waaraan je vooraf niet denkt. Als we nu van alles wat mis kan gaan ook altijd van tevoren een waarschuwing krijgen, dan kunnen we zeg maar de toekomst voorspellen. Dat klinkt misschien heel groots, maar met ons onderzoek kan dat bereikt worden. We hebben dan eigenlijk al de oplossing, voordat het probleem ontstaat en dat is wezenlijk voor betrouwbare software!”
“Heel concreet, in een aantal voorbeelden, kunnen we dus de NS helpen bij het tegengaan van seinstoringen en zelfs met het voorkomen van ongelukken op het spoor. Of kijk naar de huidige problemen met de Fyra, dat hadden we kunnen traceren, want het testen van enkel de besturingssystemen is niet voldoende, dat blijkt. Maar op andere gebieden speelt hetzelfde. Zo wordt er bij Albert Heijn altijd wel bier besteld, maar in een bepaalde periode (na carnaval) kwamen er geen bierbestellingen. Er ging toen van alles mis in hun computersysteem, wat direct invloed had op de efficiency van het bedrijf. Hadden wij daar onze analyse op toegepast, dan hadden we deze ‘bug’ in het systeem er al op voorhand weten uit te halen. Dat scheelt een organisatie een hoop tijd, geld en ergernis. We kunnen dus stellen, dat we overal waar computersystemen aan te pas komen, een voorspellend model hebben ontwikkeld en we kunnen dan ook niet wachten er volop in de maatschappij mee aan de slag te gaan”, aldus Eduardo Zambon en Arend Rensink.
Meer informatie
Op 24 januari 2013 om 16.45 uur vindt de promotie( openbaar toegankelijk) van Eduardo Zambon van de vakgroep Formal Methods and Tools van het Instituut CTIT plaats in gebouw de Waaier op de campus van de Universiteit Twente. Zijn promotor is Professor Arend Rensink (Software Modelling, Transformation and Verification) aan de faculteit EWI (Elektrotechniek, Wiskunde en Informatica). Voor meer informatie, of een digitale versie van het proefschrift ‘Abstract Graph Transformation Theory and Practice’ kunt u contact opnemen met Janneke van den Elshout, afdeling Persrelaties van de Universiteit Twente.
