Universiteit Twente (UT)-promovendus Eduardo Zambon van het CTIT Instituut voor Telematica en Informatietechnologie is gepromoveerd op een zelf ontwikkeld voorspelmodel. Met het concept wordt modelchecken mogelijk, waardoor er fouten uit systemen worden gehaald en deze systemen gegarandeerd foutvrij zijn.
Modelchecken is iets anders dan het testen van computersystemen. Bij testen kunnen wel fouten getraceerd worden in de systemen, maar het is niet te doen 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 al tien jaar onderzoek naar.
Programmeur op weg helpen
‘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 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’, vervolgt Rensink. ‘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.’
NS, Fyra en Albert Heijn
Als voorbeelden noemt Rensink de NS en de Fyra. ‘Wij hadden de NS kunnen 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 ook op andere gebieden speelt volgens Rensink 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. We kunnen dan ook niet wachten er volop in de maatschappij mee aan de slag te gaan.’
Goede systematiek is natuurlijk goud waard. Maar kijk naar wat er gebeurde met “Een methode van programmeren” van Dijkstra. Het strak hanteren van een systematische methode heeft ook aanzienlijke nadelen. Het is zoiets als 95% van de academische wereld zeggen dat ze geen wetenschap meer mogen bedrijven als het methodologisch niet verantwoord kan worden (daar zou ook veel voor te zeggen zijn).
Buiten het eventuele misverstand van een allesomvattende meerwaarde, wil ik niets bij voorbaat relativeren: als een methode daadwerkelijk ‘garbage in, garbage out’ kan voorkomen, zou dat natuurlijk goud waard zijn. Eventuele toekomstige stokpaardberijders moeten zich ook dan wel blijven realiseren, dat het niet toepassen van een methode niet bij voorbaat ‘garbage’ oplevert (daar maakten veel ICT-managers in de tachtiger jaren zich nogal eens schuldig aan).
Dus volgens de UT hoeven we straks helemaal niet meer zelf na te denken.
Het spijt me, maar ik krijg hier een onbehaaglijk gevoel bij. Het lijkt dat er sprake is van geweldige vooruitgang op het gebied van softwareontwikkeling, maar tegelijkertijd impliceert dit een achteruitgang in zelfstandig en verantwoordelijk denken en handelen, zeker als ik dat afmeet aan de genoemde praktijkvoorbeelden. Straks roept de verantwoordelijke voor de Fyra nog dat hij er niets aan kon doen omdat het systeem van de UT nog niet tot zijn beschikking stond.
Ben er nog niet uit of dit zo’n geweldige ontwikkeling is.
Er wordt in het artikel uitgegaan van een volledig getest en onfeilbaar wiskundig model. Met andere woorden: wie heeft met model getest en waarmee?
Ik kan zeker meegaan in het commentaar van Rob.
We hebben al meer aankondigingen gezien van de fundamentele wetenschap (dat ik overigens een warm hart toedraag) die de wereld compleet op zijn kop zou zetten.
Een toevoeging aan Rob’s commentaar:
1. Eerst maar eens zien wanneer het eerste concrete tool/methode beschikbaar komt voor de massa
2. Is het tool/methode te gebruiken zonder eerst te promoveren, en tot de top van een of ander vakgebied te worden, anders begrijp je de tool/methode niet
En nu maar afwachten of er bedrijven zijn die werkelijk met dit model gaan werken. Wat ik me dan wel afvraag is of het model op allerlei systemen en processen is toe te passen. Als voorbeeld in het artikel wordt de Fyra genoemd, maar is dat dan niet een brug te ver? De problemen die daarmee zijn ontstaan beperken zich niet tot software alleen, maar bestaan onder meer uit een inferieure kwaliteit van het geleverde materieel en het hoogmoedige gedrag van leverancier en NS, vooral het voor een dubbeltje op de eerste rang willen zitten. Ik vraag me af of het model dat afvangt.
Maar ik herinner me voorbeelden genoeg uit het verleden waarbij een dergelijke methode waarschijnlijk het project tot een goed einde zou hebben gebracht.
Dan rest de vraag of de toenmalige besluiten, analyses, bouwers en ontwikkelaars dan wel competent waren? Ik denk van wel, men wist niet beter, dacht alle mogelijkheden in kaart te hebben.
Het voorbeeld met het bestellen van (geen) bier bij AH vindt ik een leuke. Iets meer uitleg had het voorbeeld concreter gemaakt, nl. wat ging er mis, mochten filialen ineens geen bier meer bestellen, kon het systeem niet tegen ‘nul’ bestellingen etc. Nu er staat dat er van alles mis ging, ben ik wel nieuwsgierig wàt er dan mis ging…
De geschiedenis van IT zit vol met dit soort beloftes die komen vanuit universitaire situaties waarin de theorie wordt uitgevoerd in een speel-omgeving. Zeg, vertaalprogramma’s die perfect werken met een woordenschat van 200 woorden. En dan extrapoleren dat je het probleem alleen nog maar groter hoeft uit te voeren. In de praktijk blijken dergelijke oplossingen te leiden aan ‘combinatorial explosion’ en het schaal niet. Denk aan A-Life proponenten die suggereerden dat het kunnen evolueren van redelijke sort-algoritmen op strings van 13 bytes opschaalbaar zouden zijn naar het bouwen van passagiersvliegtuigen (de vraag negerend hoe je de ‘grim reaper’in dat geval praktisch invult.
Mijn inschatting is dat als ik het proefschrift lees, ik een situatie aantref van een kleine schaal, met beperkte vrijheidsgraden in de randcondities en daardoor een haalbaar resultaat. De mening dat je dat kunt opschalen naar een probleem als Fyra (waarvan overigens nog niet vaststaat dat er echt een structureel en onoplosbaar probleem met de treinen is) is waarschijnlijk als de grote beloftes van AI in de jaren 60 en 70: op aannames van schaalbaarheid gebaseerd die eerder geloof zijn dan wetenschap.
“Van *alles* wat mis kan gaan van te voren een waarschuwing krijgen” en dus perfecte software kan, b.v. als je in een functionele taal gaat werken. Wel eens gekeken naar de performance van dat soort omgevingen?
Als de NS specificeert dat een trein onder de 40km door rood mag rijden.
Is het model getest en goed bevonden. ICT foutloos, treinongeluk gebeurd nog steeds. Want dat is meestal de oorzaak van een treinongeluk.
Het grootste probleem van ICT zijn niet de bugs maar de specificaties..
Typische techneut oplossing. Zorgen dat de code perfect is maar niet weten of het wel wordt gevraagd…
Maar misschien is het heel handig ik wacht al tientallen jaren op zo’n model want het werd tientallen jaren geleden ook al aangekondigd…
@Corne Smiesing: Je hebt volkomen gelijk Cor.
Was het niet Barry Boehm die al enkele decennia geleden aantoonde dat er in de specificaties meer fouten voorkwamen dan in de opgeleverde software?
Niettemin, elke verbetering van het ontwerp en bouwproces is natuurlijk welkom maar blijf met beide benen op de grond staan: fouten blijven voorkomen
Corne, je haalt me de woorden uit de mond. Buiten het feit dat ik me afvraag of ooit iets foutloos kan zijn, stel ik me altijd gelijk de vraag wat foutloos nu precies is.
Je ziet in dit artikel en de reacties dat het een semantische discussie wordt, en de inhoud als een academisch discussie wordt gezien die de werkelijke wereld niet echt raakt.
Nog sterker, fouten zijn volgens mij de basis tot vooruitgang. In een foutloze wereld is als volgens het geen een ieder wil. Deze 2 uitgangspunten kan ik me een hoge waarschijnlijk verwerpen als waar, kortom, het artikel heeft een paar foutjes in haar uitgangspunten ergo…
Mickel slaat de spijker op zijn kop. Van fouten leren we en komen we uiteindelijk verder.
Foutloze ICT zou tevens erg saai zijn en er zou ook minder voor ons allen te doen zijn.
Dus laten we hopen dat het niet die kant op gaat.