Softwarebetrouwbaarheid

Software is een onmisbaar onderdeel geworden van ons dagelijks leven. We kunnen ons niet meer voorstellen hoe het leven zou zijn zonder mobiele telefoon en alle applicaties die alles zoveel makkelijker maken. Maar ook in allerlei andere aspecten van ons dagelijks leven speelt software een cruciale rol: auto’s zijn rijdende computers geworden, stoplichten en treinen worden gecontroleerd door software, tijdens operaties worden chirurgen ondersteund door operatierobots en bedrijven doen hun voorraadbeheer en administratie tegenwoordig volledig digitaal. Voor al deze toepassingen is het belangrijk dat software betrouwbaar is, en ook daadwerkelijk doet waar het voor bedoeld is. Daarom wordt er al sinds de jaren 60 onderzoek gedaan naar technieken om de kwaliteit van software te kunnen garanderen. In eerste instantie waren dat vooral technieken om met pen en papier over de kwaliteit van een computerprogramma te kunnen redeneren, maar later werden er ook speciale programma’s ontwikkeld die de softwareontwikkelaar konden helpen om garanties te geven over de kwaliteit van de software. Het ontwikkelen van dit soort programma’s is de basis van mijn onderzoek.

Toen ik begon met mijn onderzoek naar het ontwikkelen van programma’s die helpen om de softwarebetrouwbaarheid te verbeteren, vond ik het belangrijk om technieken te ontwikkelen waarmee het mogelijk is om te laten zien dat software 100 procent correct is, en in alle omstandigheden zich precies zo gedraagt als gewenst. Samen met mijn collega’s in Nijmegen ontwikkelde ik tijdens mijn promotieonderzoek verificatietechnieken waarmee je het gedrag van computerprogramma’s heel precies kunt analyseren, en uitspraken kunt doen over alle mogelijke gedragingen van een programma. Deze technieken implementeerden we dan weer in onze speciale controleprogramma’s en we gebruikten ze om de correctheid van allerlei kleine maar complexe programma’s te laten zien.

Het werk uit die tijd heeft veel invloed gehad en is gebruikt om de correctheid van allerlei complexe algoritmen aan te tonen. Na verloop van tijd realiseerde ik me echter dat om 100 procent correctheid te kunnen garanderen, er heel veel extra werk nodig is van de softwareontwikkelaar. De broncode van het computerprogramma moet geanalyseerd worden en allerlei speciale instructies moeten toegevoegd worden, die gebruikt kunnen worden om met behulp van het door ons ontwikkelde controleprogramma de precieze garanties over de software af te kunnen leiden. Om dit te kunnen doen, moet de softwareontwikkelaar niet alleen weten wat het programma moet doen, maar ook hoe de analysetechnieken werken. En zelfs als hij of zij dat weet, dan kost het veel tijd om al dit extra werk te doen. Daarbij komt: hoe groter het programma, hoe meer tijd het kost. Deze tijd is er vaak niet en het wordt ook steeds lastiger om dit te doen, omdat software steeds groter en complexer wordt.

Maar gelukkig is er hoop, want ik realiseerde me ook dat het niet altijd nodig is om 100 procent garantie te kunnen geven over het gedrag van de software. Voor veel van de programma’s die we dagelijks gebruiken, is het vervelend als er iets misgaat, maar geen ramp. De app crasht, we moeten deze opnieuw opstarten en daarmee is het probleem meestal opgelost. Voor sommige softwaretoepassingen is de correctheid wel essentieel. Denk bijvoorbeeld aan de software die het treinverkeer controleert: het blijft essentieel dat seinen en overwegbomen correct werken… Maar de code die hier voor zorgt, is vaak maar een klein onderdeel van het grote programma, en het is voldoende om alleen naar dit stukje code te kijken en 100 procent garantie te geven.

Daarnaast realiseerde ik me dat de technieken die we tot nu toe altijd gebruikt hadden om deze 100 procent correctheidsgarantie te geven ook op een andere manier ingezet konden worden. Ook als de softwareontwikkelaar minder werk doet, en alleen de code schrijft, maar niet allerlei extra instructies, is het mogelijk om de door ons ontwikkelde technieken en controleprogramma’s te gebruiken om snel fouten in de software te vinden. Dit zijn dan geen fouten die er voor zorgen dat de software iets verkeerd doet, maar wel de fouten die ervoor zorgen dat de software crasht of vastloopt. Als we dit soort fouten op een makkelijke en efficiënte manier kunnen detecteren, dan is het daarna ook makkelijker om te controleren dat de software niet alleen niet crasht, maar ook nog eens het juiste doet. Daarom richt ik me tegenwoordig in mijn onderzoek niet alleen meer op complexe software die ingewikkelde berekeningen doet, maar kijk ik ook naar hoe we softwareontwikkelaars kunnen helpen om zo snel mogelijk kleine foutjes in hun code te ontdekken.