Geautomatiseerde controle zal softwarekwaliteit sterk verbeteren

Bij het Centrum Wiskunde & Informatica (CWI) is eind vorig jaar Alexandra Silva gepromoveerd op automatische controle van softwarekwaliteit met behulp van specificatietalen die afgeleid zijn uit de logica. Door deze voorziening de komende jaren in te bouwen in programmeerhulpmiddelen zal de kwaliteit van software sterk verbeteren.

Silva ontwierp een universeel raamwerk, Kleene coalgebra, waarmee uit de logica afgeleide specificatietalen automatisch gegenereerd kunnen worden. Zij verdedigde haar proefschrift 'Kleene Coalgebra' op 21 december 2010 aan de Radboud Universiteit Nijmegen en kreeg daarvoor het predicaat 'cum laude'. In de toekomst kan haar onderzoek gebruikt worden voor het verbeteren van de kwaliteit van software, bijvoorbeeld bij het ontwerp van elektronische circuits. Het is een belangrijke stap omdat software in veiligheidskritische systemen nu soms nog fatale fouten bevat.

Een bekend voorbeeld dan zijn de softwarefouten in het Therac-25 bestralingsapparaat waardoor in de jaren '80 meerdere patiënten overleden. Een ander bekend voorbeeld is het exploderen van de Ariane 5-raket dat ook toegeschreven werd aan een fout in de software. Om dit soort rampen in de toekomst te voorkomen, vertalen theoretisch informatici computersystemen in een wiskundig model dat ze vervolgens testen. Deze stap is nodig omdat het oorspronkelijke systeem vaak te complex is om in zijn geheel te testen. Tussenkomst van een model zorgt ervoor dat die complexiteit vermeden kan worden. Silva voegde een grote klasse modellen aan haar Kleene Coalgebra-raamwerk toe, waarvoor ze in staat was om zowel de specificatietalen als axiomatisaties te genereren.

Het promotieonderzoek van Silva is gefinancierd door FCT (Fundação para a Ciencia een Tecnologia) in Portugal, en is uitgevoerd onder auspiciën van IPA (Institute for Programming research and Algorithmics) in Nederland. Silva gaat nu als postdoc-onderzoeker in de Foundations of Software Engineering groep (SEN3) op het CWI hulpmiddelen maken voor haar framework, zodat haar onderzoek in de praktijk toegepast kan worden. Het is de verwachting dat toepassing van deze technieken door programmeurs de komende jaren de softwarekwaliteit sterk zal verbeteren.