Applicaties die nooit meer vastlopen
Je belastingsaangifte, Netflixen of autorijden: steeds meer dagelijkse activiteiten worden ondersteund door computerapplicaties. En omdat het zo moeilijk en duur is om software grondig te testen, zitten er in de meeste applicaties fouten. Promovendus Benjamin Lion maakte een wiskundig framework om dit probleem aan te pakken. Met het framework kan hij aan de hand van wiskunde uitsluiten dat het gebruik van bepaalde software zal leiden tot onvoorziene fouten. Dat kan helpen bewijzen dat het gebruik van bepaalde software niet leidt tot onvoorziene fouten. Hij promoveert op 1 juni.
Je wilt een van je favoriete tv-programma's aanzetten, maar het programma weigert te starten zonder duidelijke reden. Of je speelt een spelletje op je smartphone en plots loopt het vast. Gebeurt het je ook wel eens? In de meeste software zitten er af en toe fouten, al werkt het gelukkig meestal wel goed.
Onvoorziene fouten treden vooral op wanneer software voortdurend moet communiceren met de wereld waarin wij leven. Denk bijvoorbeeld aan de besturingssystemen van zelfrijdende auto's. Dat komt omdat het moeilijk is om software te testen in een realistische simulatie van de wereld waarin we leven. ‘Een goede manier vinden om natuurkunde en cyber te combineren, is een hele uitdaging’, aldus promovendus Lion. Hij ontwierp een wiskundig framework om deze kloof te overbruggen, dat het mogelijk maakt om software grondiger te testen.
Een parkeerplaats met zelfrijdende auto's indelen
Met zijn framework kan Lion wiskundig bewijzen dat software geen fouten bevat als het in een bepaalde fysieke omgeving wordt gebruikt. Hij testte het framework met succes voor een hypothetische situatie: 'Ik gebruikte het voor een parkeerplaats met zelfrijdende auto's die ik opnieuw wilde indelen. De auto's hebben allemaal bepaalde eigenschappen, bijvoorbeeld dat ze niet tegelijkertijd op één plaats kunnen zijn. En ze hebben accu's die niet leeg mogen raken.' Met een beschrijving (de software) van de auto's en de parkeerplaats (de omgeving), controleert het framework op basis van de wetten van de natuurkunde of de code fouten bevat. 'Of de auto's tegen elkaar kunnen botsen bijvoorbeeld.'
Door software beter te testen aan de hand van wiskundige methoden, is dit probleem mogelijk opgelost.
De klassieke manier om software te testen voor het herschikken van zelfrijdende auto's op een parkeerplaats, zou zijn om mogelijke scenario's te bedenken die tot fouten kunnen leiden. Die scenario's kunnen dan in een simulatie worden getest. Helaas is het voor een programmeur onmogelijk om alle scenario's in kaart te brengen die mogelijk tot fouten in de software kunnen leiden. Door software beter te testen aan de hand van wiskundige methoden, is dit probleem mogelijk opgelost.
De uitdagingen van meerdere auto's tegelijkertijd
Wat het framework van Lion vooral interessant maakt, is dat het kan dienen om te controleren of meerdere auto's - of meerdere stukken software - zonder fouten op elkaar kunnen inwerken. 'Elke auto bevindt zich in een andere positie en staat in verschillende richtingen. Daarom registreren ze verschillende dingen aan en bewegen ze op andere momenten.' Een belangrijke uitdaging voor Lion was het weergeven van 'tijd'. Lion: 'In het echte leven is tijd continu. Iets kan op elk moment veranderen. Maar een computer werkt in discrete stappen.' Dat betekent dat iets kan gebeuren op de tel van één, of twee, enzovoort, maar niet op elk moment daartussen.
Deze afwijkende weergave van tijd in de cyberomgeving kan leiden tot onvoorziene fouten zodra de software interactie heeft met de fysieke wereld. Auto's zouden tegen elkaar kunnen botsen als ze op iets andere momenten hun acties veranderen. Dit is wat onderzoek waarbij de cyber- en fysieke wereld op nieuwe manieren met elkaar worden verbonden zo belangrijk maakt, aldus Lion: 'Het geeft nieuwe inzichten om te begrijpen hoe de theorie van de berekenbaarheid (wat een machine kan doen) zich verhoudt tot de theoretische natuurkunde (de mogelijkheden van de natuur)Deze kan ons helpen om beter te begrijpen hoe machines interageren met de fysieke wereld. En daardoor kunnen we vervolgens betere cyber-fysische systemen ontwerpen.'
Tekst: Merel Wiersma