Foutenvrije computerprogramma’s dankzij wiskunde en logica

Wat zou het mooi zijn als programmeurs bij het schrijven van software een autocorrect-functie hadden, die fouten aanwijst een verbeteringen voorstelt! Jorge Pérez, adjuncthoogleraar Software Foundations aan de RUG, gebruikt wiskunde en logica om te komen tot een wereld zonder softwarefouten. Een wereld waar programma’s niet meer vastlopen en belangrijke instanties zoals ziekenhuizen en luchthavens nooit meer hoeven te sluiten wegens slecht werkende programma’s, zoals afgelopen jaar.

 FSE Science Newsroom | René Fransen

‘Software fouten kunnen veel geld kosten, en zijn soms rampzalig’, zegt Pérez. ‘Maar programma’s schrijven die helemaal kloppen is lastig, zelfs voor ervaren programmeurs.’ Al tientallen jaren testen zij daarom hun software om fouten op te sporen. Alleen is dat niet voldoende: ‘Met testen kun je fouten vinden, maar je kunt niet garanderen dat er geen fouten meer in de software zitten.’ En omdat software tegenwoordig overal in zit kunnen fouten in programma’s allerlei onvoorziene gevolgen hebben.

Multitaskende software, foutloos ontworpen

Wat het extra uitdagend maakt is dat moderne software allerlei opdrachten tegelijkertijd moet kunnen uitvoeren, iets dat concurrency (gelijktijdigheid) heet. Webshops gebruiken het om te zorgen dat heel veel klanten tegelijkertijd producten kunnen zoeken, afrekenen of beoordelen. ‘Concurrency is geweldig, daardoor werken onze telefoons en laptops zo snel. Maar dit soort programma’s is moeilijk te schrijven, omdat wij mensen nu eenmaal denken in stapjes, waarin taken na elkaar komen.’

Dit maakt het lastig voor software bouwers om de gelijktijdige processen op de juiste manier te programmeren, ze moeten anticiperen welke van die taken gelijktijdig kunnen plaatsvinden. Pérez gebruikt wiskunde en logica om uit te zoeken hoe goed taken worden uitgevoerd in zo’n complexe situatie. ‘Door de correctheid op een wiskundige manier te beschrijven kunnen we precies omschrijven wat het doel is van de verschillende instructies in een programma. Daardoor kunnen we controleren of die instructies, en uiteindelijk het hele programma, dat doel ook bereiken.’ Pérez is gespecialiseerd in wiskundige modellen van programma’s die concurrency gebruiken. ‘De modellen gebruiken we om te bepalen hoe realistisch het is dat deze programma’s zonder fouten werken.’

Die aanpak helpt de ontwikkeling van nieuwe methoden om subtiele programmeerfouten te elimineren. ‘Het mooiste zou zijn wanneer we iets kunnen bouwen zoals de autocorrect functie in Google Docs, die fouten aanwijst en verbeteringen voorstelt’, zegt Pérez. Maar hoewel computertalen beperkter zijn dan gewone taal is dat nog niet zo eenvoudig. ‘Softwaresystemen zijn complex: ze worden gebouwd door verschillende programma’s te integreren, een beetje zoals je met Lego bouwt. Bovendien zijn die programma’s groot, lopen ze op verschillende computers verspreid over de wereld en gebruiken ze verschillende technologieën. Deze complexiteit pakken we aan door zeer strikte methoden te ontwikkelen waarmee programma’s geschreven worden die vanaf de ontwerpfase foutenvrij zijn. Dat was het onderwerp van mijn VIDI project.’

Samenwerking en publieke optredens

Pérez werkt aan deze problemen met zijn studenten en met collega’s van de Fundamental Computing groep, maar ook binnen een samenwerkingsverband van Nederlandse computerwetenschappers, NetTCS. En hij beperkt zich niet tot vakgenoten, maar betrekt ook een breed publiek bij zijn onderzoek naar foutenvrij software. ‘Ik ben vooral trots op een lespakket voor middelbare scholen dat ik heb gemaakt in samenwerking met de Scholierenacademie van de RUG.’ Via het lespakket kunnen scholieren leren hoe software werkt en wat er fout kan gaan. ‘Verder geef ik presentaties op wetenschapsfestivals zoals Noorderzon, en ik heb een aantal video’s gemaakt over het belang van het controleren van software op fouten.’

Zijn benadering kan de betrouwbaarheid van complexe software systemen vergroten. Zal dit uiteindelijk leiden tot programma’s zonder fouten? ‘Dat is mijn ultieme doel’, zegt hij. ‘Ik denk ook dat wij als computerwetenschappers de verantwoordelijkheid hiervoor hebben.’ Dat lijkt een erg zware taak, maar Pérez deinst er niet voor terug: ‘De toekomst is opwindend. We zijn steeds sterker bewust van het belang van betrouwbare software voor de maatschappij. En de industrie is ook in toenemende mate geïnteresseerd in wiskundig getoetste software.’

Zie ook de website van Jorge Pérez, en zijn volledige CV.