Van cruciale fouten in de software in kritieke infrastructuur als dijken en bruggen tot een vastloper tijdens een spelletje op de laptop: softwarefouten zijn er in alle soorten en maten. Niet altijd desastreus, maar vaak wel hinderlijk. Hoe komen we zo dicht mogelijk bij foutloos werkende software?
Dat het antwoord van goedwerkende software ligt in correct programmeren en adequaat testen en verifiëren, lijkt een open deur. Maar de stappen die daarvoor nodig zijn, zijn heel wat complexer. Zeker met de toenemende complexiteit van soft- en hardware. Prof. dr. Marieke Huisman, professor Software Reliability, gaf tijdens haar oratie op donderdag 25 januari een inkijkje hoe verbetering van de dagelijkse praktijk van softwareverificatie moet leiden tot een grotere betrouwbaarheid van alle software.
Gedegen stappenplan
Goede verificatie vraagt in de eerste plaats om goed te beschrijven welke eigenschappen we er eigenlijk van verwachten, stelt Huisman. In het expliciteren van systeemverwachtingen, op een formeel correcte wijze en eenduidig, is nog een wereld te winnen: een cruciale stap om in complexe processen te kunnen verifiëren of de software ook daadwerkelijk doet waarvoor het gemaakt is.
De verdere verfijning van softwareverificatie vraagt om nauwe samenwerking tussen en binnen wetenschap en het werkveld, om zorg te dragen dat een bredere inzetbaarheid van verificatietechnieken wordt bewerkstelligd. “We moeten ons bijvoorbeeld richten op het ontwikkelen van redeneertechnieken die makkelijk uit te leggen en toe te passen zijn”, aldus Huisman. “Zodat niet alleen experts (dat wil zeggen de onderzoeker die de techniek ontwikkeld heeft) deze kunnen gebruiken, maar ook softwareontwikkelaars.”
Ook ligt er een grote uitdaging op het gebied van samenwerking en integratie van verificatieprogramma’s. Huisman: “Op het moment is het gebruik van resultaten van één programma in een ander programma zwaar werk, waar veel aan geprogrammeerd moet worden. Als programmaverificatie-gemeenschap moeten we veel meer inzetten op hergebruik en samenwerking.”
Onderzoek én onderwijs
Het vergroten van de betrouwbaarheid van software is niet alleen een onderzoeksopgave. Juist ook in het onderwijs kunnen daarin grote stappen worden gezet. Huisman: “Er is een andere aanpak nodig is, waarbij studenten al heel snel ervaren dat het mogelijk (en noodzakelijk) is om precies op te schrijven wat een stukje code doet en om alle impliciete aannames expliciet te maken. Vervolgens moeten we dan proberen om studenten zelf te laten ervaren dat wat zij daar hebben opgeschreven daadwerkelijk helpt om fouten te vinden en hun programma beter te maken. Om dat te bewerkstelligen is het niet noodzakelijk om dit verplicht te maken, wel om dit vanaf het begin af aan mogelijk te maken en om dit op zo’n manier te doen dat de studenten ook daadwerkelijk de voordelen kunnen ervaren. Daarom moet er een ontwikkelomgeving zijn die snelle feedback kan geven en die gebruikers uitdaagt om steeds meer uit het systeem te halen, bijvoorbeeld door gamificatie: hoe meer specificaties er geschreven en gevalideerd worden, hoe meer punten er verdiend kunnen worden.”
Over Marieke Huisman
Marieke Huisman promoveerde in 2000 aan de Radboud Universiteit op de verificatie van sequentiële programma’s (in het bijzonder Java) en is sinds 2008 werkzaam aan de Universiteit Twente. In 2010 verkreeg ze een Starting Grant van de Europese Research Council (ERC), waarmee ze de ontwikkeling van VerCors inzette: een toolset van verificatietechnieken voor concurrent datastructuren. In 2013 ontving ze de Nederlandse prijs voor ICT-onderzoek, en vorig jaar kreeg ze een Vici-beurs uitgereikt door de Nederlandse Organisatie voor Wetenschappelijk Onderzoek (NWO).
Sinds september 2017 is Huisman voorzitter van het Ambassadeursnetwerk, dat is ingesteld door het College van Bestuur met als taak te adviseren over maatregelen die de doorstroom van vrouwen naar hogere posities bevorderen.
