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.’
Gezien de reacties die hier voorbijkomen wordt er te zwaar getild aan deze aankondiging. Natuurlijk kan geen enkele methode of tool ervoor zorgen dat software voor 100% doet wat het moet doen. Wat eerder al werd gezegd: dat is afhankelijk van de specificaties.
Waar dit onderzoek en deze resultaten over gaan is de volledigheid van het testen van dergelijke specificaties. Ik heb zelf bij mijn afstuderen ook gewerkt aan de Groove-tool en deze stelt een ontwikkelaar (of tester) in staat om voor een gegeven specificatie *alle* mogelijke situaties in een stuk software door te rekenen. Dit betekent effectief dat er dus gegarandeerd een 100% coverage uit voor de tests ontstaat.
De kwaliteit van de software hangt dan natuurlijk nog steeds af van hoe goed de specificaties zijn geformuleerd. Het helpt in ieder geval bij het opsporen van die randgevallen, die vaak lastig zijn te voorspellen en dus wel eens buiten de boot vallen bij het testen.
Ik ben benieuwd of deze tool en aanpak ondertussen al geschikt zijn om zakelijke applicaties mee te analyseren en meld mij bij deze graag aan voor een testtrajectje 🙂
Wordt er vanuit gegaan dat de specificaties volledig juist zijn? Een illusie lijkt me. En hoe kijkt men aan tegen ontwerpgebreken?
Ik vermoed dat de voorgestelde benadering uit moet gaan van een gesloten systeem – hoe kun je anders de integratie tussen applicatiesoftware, systeemcomponenten en infrastructuur beheersen?
Testen is in veel gevallen onmisbaar.
Vraag aan Jan Hendrik Kuperus:
Is het ook mogelijk om te testen of b.v. een webservice nog performed bij 1000 gebruikers tegelijk? Want ik denk dat Marktplaats er dan wel interesse in heeft.
En hoe om te gaan met webbased software?
Ik ben serieus geïnteresseerd of hiervoor dan ook een oplossing is.
Voor de fans. De thesis staat ook op internet:
http://eprints.eemcs.utwente.nl/22860/
Ik begrijp uit het verhaal iets heel anders dan de titel van dit artikel verkondigt.
Voor zover ik kan overzien meent Zambon aan te kunnen tonen of een bepaald proces foutloos kan verlopen.
Wiskundig bewijzen dat een programma ten alle tijde correct werkt is al langer mogelijk, maar daar zijn wel voorwaarden aan verbonden.
Dit is nog geen foutvrije ICT. immers daarvoor moeten alle deelsystemen ook foutvrij of anders 100% betrouwbaar zijn.
Lijkt me nogal hachelijk als iemand durft te beweren dat een heel kantoornetwerk en daarmede de ICT omgeving van dat kantoor foutvrij is.
Prachtig, zo’n wiskundig model, maar in de praktijk moet ik nog zien of het zijn waarde zal bewijzen.
Ik zie al aankomen dat we straks mathematisch perfecte systemen hebben waar geen bugs inzitten vanuit programmatechnisch oogpunt, maar die toch volledig onbruikbaar zijn omdat de grilligheid van gebruikerswensen nu eenmaal zeer moeilijk zoniet onmogelijk te vangen is in een wiskundig model. Vooralsnog ben ik redelijk sceptisch t.o.v. een dergelijk model in de werkelijke praktijk in tegenstelling tot de academische praktijk, welke nog wel eens de neiging heeft anders te zijn.
Het artikel onderschrijft ook niet de pretentieuze kop, maar geeft wel aan dat er modellen te maken zijn die HELPEN bij het duiden en filteren van technische oneffenheden. Het artikel geeft duidelijk aan dat het voorkomen van alle funktionele tekortkomingen in software ondoenlijk is. Niet door gebruikers en laat staan door IT-ers. Precies zoals verwoord door Corne Smiesing, met max. 40 kmh mag een trein door een rood sein rijden.
Verder weet natuurlijk elke T-mapper dat er scripts te ontwikkelen zijn per funktionaliteit om foutenreductie te bewerkstelligen. Maar de ideale wereld bestaat niet, processen en procedures zijn mensenwerk. Denk hierbij aan rollback scenario bij een release update en denk hierbij aan de recente web applicatie update bij het UWV (1 volle week niet beschikbaar na release update). Dit is een typisch ITIL/PRINCE2 issue door menselijk handelen. Soms is een rollback de duur en word het risico vooraf aanvaard door management (als ze het snappen en/of op de hoogte zijn gebracht), door de EN NU KOMT HET de ‘WAARSCHIJNLIJKE’ gevolgen en risico’s te aanvaarden en in te calculeren. Dit berust dus op aannames en aannames zijn levensgevaarlijk. Uit veel commentaar maak ik op dat de UT zou uitgaan van aannames maar dat blijkt uit de rest van het artikel niet.
NIAM pretendeert al jaren foutloze systemen te kunnen modelleren. En het werkt als je je aan alle voorschriften houd, maar commercieel niet interessant er gaat (te) veel tijd in het ontwerp zitten, het technisch ontwerp en de uitvoering zijn beduidend goedkoper, maar een trechtermodel is commercieel veel interessanter
Mooie reactie Oskar. Mee eens.