Development

Software-ontwikkeling
Frisse blik: ‘Groot gat tussen wetenschappelijke oplossing en praktische toepassing’

Frisse blik: ‘Groot gat tussen wetenschap en praktische toepassing’

PhD-onderzoeker hoopt dat toepassen van formele methoden makkelijker wordt voor groter publiek.

21 mei 2020

PhD-onderzoeker hoopt dat toepassen van formele methoden makkelijker wordt voor groter publiek.

Soms is het testen van softwareprogramma’s niet voldoende om geen softwarefouten in de code te garanderen. Verificatie van software biedt een betere garantie, zegt Sophie Lathouwers, PhD-onderzoeker aan de Universiteit van Twente. Toch wordt de techniek amper in de industrie toegepast. En dat is jammer, vindt Lathouwers. Zij richt haar onderzoek op de praktische toepasbaarheid van verificatie.

Een voorbeeld dat Lathouwers noemt is de problemen die vliegtuigbouwer Boeing had met de 737 MAX. Op het controleproces van de vliegtuigbouwer komt vanuit verschillende kanten kritiek. “Het is aannemelijk dat Boeing door verificatie softwareproblemen had kunnen voorkomen”, zegt ze.

Maar het is nu eenmaal zo dat veel waar de wetenschap aan werkt, niet wordt toegepast in het bedrijfsleven. “In de wetenschap wordt aan veel problemen gewerkt en zijn er veel technieken die krachtig zijn. Maar vaak is zo’n techniek niet in een bruikbare vorm beschikbaar voor de industrie. Dat er nog zo’n gat zit wat er in de wetenschap aan onderzoek gebeurt en wat in de industrie wordt toegepast, dat blijft me verbazen.”

Verificatie, het onderzoeksgebied waar Lathouwers, is ook nog niet ideaal toepasbaar voor de industrie. Bij verificatie geeft je antwoord op de vraag of het systeem voldoet aan de specificatie. Lathouwers: “Net als dat je bij wiskunde fouten opspoort door formules te toetsen, kun je dat ook voor een softwareprogramma doen. Dat heet deductieve verificatie. De specificatie van de code schrijf je in formele taal uit. Daarna beredeneert de computer of de code werkt zoals hij zou moeten.” Om verificatie toe te passen, moet de code goed begrepen worden. Bovendien is het een tijdrovend proces. “Ik ben nu bezig met het verifiëren van het Dijkstra-algoritme om het kortste pad te vinden. Ik ben nu twee tot drie weken bezig en het is nog niet af. Natuurlijk ben ik ondertussen aan het leren maar het ook zonder dat je dat doet, kost verifiëren wel echt veel tijd. Eerder heb ik een lowlevel algoritme geverifieerd en daar ben ik twee weken mee bezig geweest.”

Lathouwers onderzoekt daarom hoe softwareverificatie beter toepasbaar kan worden gemaakt voor de industrie. “Softwareverificatie is een academisch idee. Natuurlijk wordt het wel in bepaalde gevallen toegepast, bijvoorbeeld door ESA. Maar voor software waarbij de impact van de fout minder groot is, is de vraag of het de tijd, kosten en energie wel waard is.”

Waarom koos je voor onderzoek naar dit onderwerp?

“Zowel mijn bachelor- als masterstudie heb ik gedaan aan de Universiteit van Twente. Daar kwam ik ook prof. dr. Marieke Huisman tegen bij wie ik mijn promotieonderzoek nu doe. Zij houdt zich bezig met verificatie. Toen ik in het tweede jaar van mijn studie te maken kreeg met deze techniek, wilde ik daar meer over weten. Verificatie is het volgen van logische stappen op basis van hardcore informatie die eronder ligt. De methode is gebaseerde op wiskundige methoden. En ik hou van die wiskundige kant van informatica.”

Wat is lastig aan jouw onderzoek?

“Eigenlijk zou je met een magische berekening willen kunnen zeggen of software correct is. Dat kan helaas niet. Software is te complex. Natuurlijk kun je wel op onderdelen zeggen dat dingen niet kunnen. Bijvoorbeeld op gebied van het geheugenbeveiliging dat je maar maximaal twee berekeningen tegelijk mag uitvoeren. Dat onderdeel valt redelijk te automatiseren. Maar functionele correctheid uitvoeren valt niet volledig te automatiseren, het zal dus altijd een tijdrovend proces blijven.”

Waar zitten de uitdagingen?

“Praktisch maken van wat ontdekt is, bijvoorbeeld het genereren van specificaties. Voordat de techniek echt goed toepasbaar is, moet het schaalbaar zijn. En dat is het nu niet. De industrie heeft miljoen regels aan code. En dat is lastig om goed verificatie op toe te passen.”

Waar verwacht je veel van?

“Als we formele methoden bruikbaarder kunnen maken voor de mensen die niet zoveel van de theorie erachter weten, kan het ervoor zorgen dat meer mensen het gaan gebruiken. Denk bijvoorbeeld aan een betere interactie met tools door de interfaces die worden gebruikt. Waardoor het makkelijker wordt om gebruik te maken van verificatie voor software. Verificatie zou best meer kunnen worden toegepast, maar het aantal mensen dat het gebruikt is nu nog beperkt.
Ik denk dat het komt omdat mensen nu nog te veel moeten begrijpen van de theorie om het goed te kunnen gebruiken. Als ik bijvoorbeeld specifiek naar het onderzoek kijk waar ik nu mee bezig ben, dan moet je eerst de specificatie omschrijven naar logica en dan pas kun je de formele methode toepassen. Ik ben nu bezig om te onderzoeken hoe we specificaties in een normale taal kunnen omzetten naar logica. Dan wordt voor een gebruiker de drempel al lager gelegd.”

Naar welke ontwikkeling ben je nieuwsgierig?

“Of verificatie in de toekomst meer door bedrijven wordt toegepast. Ik denk het niet, omdat het niet voor alle bedrijven even nuttig is. Voor de software van een webshop is het te tijdrovend, maar voor een Boeing kan het problemen voorkomen. Ik verwacht dat in de toekomst vooral een specifieke groep bedrijven verificatie zal gebruiken. Maar ik denk dat het lang gaat duren.
Eigenlijk gaat er bizar veel goed als je kijkt hoeveel software er wordt gebruikt. En dat zorgt voor een extra drempel naar verificatie, testen blijkt vaak ook voldoende te zijn.”

Hoe denk je dat de toekomst er uit komt zien van softwareverificatie?

“Verificatie wordt nu nog beperkt gebruikt, maar dat zal wel meer worden. Omdat het relatief heavy-weight oplossing is om te zorgen dat je geen fouten in het programma hebt, is het vooral toepasbaar voor high risk applicaties. Denk aan een securitytoepassing, in zelfrijdende auto’s of in vliegtuigen.
Er zijn nog wel een aantal praktische problemen, zoals het gebruiksgemak, maar ook dat sommige technieken veel tijd kosten om een verificatie uit te voeren. Daarom denk ik dat verificatie vooral zal worden toegepast voor het belangrijkste deel van het systeem, bijvoorbeeld de kernel van een operatingsysteem. Maar voordat dit echt gaat gebeuren, zijn we wel 20 jaar verder, denk ik.”

Weet je al wat je in de toekomst wilt gaan doen?

“Dat weet ik nog niet. Mijn masteronderzoek heb ik bij een bedrijf gedaan: Northwave, een securitybedrijf. Ik wilde ook weten waarom verificatie niet veel wordt gebruikt in het bedrijfsleven. En ik heb me verdiept in het securityvakgebied. Het was een interessante periode, maar ik besloten om voorlopig weer onderzoek te doen. Wel praktisch onderzoek. Ik vind het belangrijk om het nut van mijn onderzoek in te zien. Zo hou ik mezelf gemotiveerd.”

Lees meer over Development OP AG Intelligence
2
Reacties
Eric-Jan Hoogendijk 23 mei 2020 10:42

Ik geef het je te doen: No Code -> HLL1 -> HLL2 -> Assembler -> MachineInstruction -> Elektrische schakeling op de CPU-chip. En dan nog alle firmware in de aan te sturen devices en het OS; elke stap zal formeel getoetst moeten worden.

IBM was in de jaren 90 niet blij toen ik zei dat hun nieuwe Low Code taal Cross Systems Product verkeerde Cobol als tussentaal genereerde. Wat er dan fout was vroegen ze. Ik antwoorde formeel dat wij geen Cobol kende en dat ze dit ook niet aan ons zouden vragen wanneer Cobol verkeerde Assembler zou genereren. Het duurde even voordat het kwartje bij hen viel.

Atilla Vigh 22 mei 2020 12:22

Als dit hetzelfde is als ik tijdens mijn studie heb mogen ontvangen, zou betekenen dat we 30 jaar zijn blijven stil staan. Formele methoden, waarbij je met pre- en postcondities in een pseudo taal de toestand van een automaat beschrijft werd toen al als basis voor correcte algoritmiek. En als we nu nog niet in staat zijn om het kortste pad algoritme van Dijkstra formeel te toetsen, vraag ik me af of 20 jaar niet een beetje te optimistisch is. Ik hoop stiekem dat we verder zijn in de wetenschap.
Overigens naast de formele toetsing van het algoritme, zit er nog een gat tussen de pseudo-taal en de uiteindelijke implementatie in een echt computersysteem. Omdat wij onze complete ICT-Infrastructuur gelaagd hebben opgebouwd, zitten er tussen de implementatie van bewezen stukje code en de rest (in de stack) heel veel afhankelijkheden. Deze afhankelijkheden zijn juist vaak debet dat er toch iets niet gaat werken. De complete stack (van firmware tot UI) testen met formele methoden met al zijn afhankelijkheden is de heilige graal. Of dat ooit te bereiken is?

Reactie toevoegen
De inhoud van dit veld is privé en zal niet openbaar worden gemaakt.