Promovendus Thomas Arts introduceert een techniek waarmee in principe alle eigenschappen van softwareprogramma’s automatisch zijn aan te tonen. Wiskundige modellen die informatie geven over de bedrijfszekerheid van software voordat deze echt gebouwd is, zouden complexe en dure testprogramma’s deels kunnen vervangen.
Thomas Arts van de Universiteit Utrecht is onlangs gepromoveerd op zijn proefschrift Het automatisch bewijzen van terminatie en innermost normalisatie van termherschrijfsystemen. Hij toont aan dat ook zonder ingewikkelde en vaak kostbare testprogramma’s zekerheid over het gedrag van software te verkrijgen valt.
Veel softwareprogramma’s zijn niet echt betrouwbaar. Gebruikers merken regelmatig dat het aangeschafte pakket zich op onderdelen anders gedraagt dan de leverancier aangeeft. Nu zijn er fouten en fouten. Fouten in tekstverwerkers zijn vervelend. Bugs in kritische softwaresystemen, bijvoorbeeld voor vliegtuigen of kerncentrales, kunnen desastreus zijn.
Leveranciers proberen met testen fouten zoveel mogelijk op te sporen. Testprogramma’s hebben echter beperkingen. Een grote beperking is dat niet oneindig naar fouten gezocht kan worden. De markt wil nu eenmaal vaak dat een nieuw programma snel wordt geïntroduceerd. Het is in de praktijk ondoenlijk om alle mogelijke invoer en alle randcondities te testen en te verwerken. Als een test geen bugs aantoont, betekent dat dus niet dat er ook geen fouten zijn.
Wiskundig
Een andere beperking van testprogramma’s is dat ze fysiek over een geïmplementeerd programma moeten beschikken. Testen kan tot nu toe alleen maar nadat de software is ontwikkeld en geschreven. Vergeleken met andere branches is zo’n testmethode achterlijk. Men bouwt toch immers ook niet eerst een brug om, nadat hij is ingestort, de constructie te veranderen.
Een architect die wil bewijzen dat een brug sterk genoeg is, stelt er een wiskundig model van op. Binnen dat model kan hij de sterkte van de brug berekenen. Arts geeft aan dat zo’n methode ook toepasbaar is voor software. Mathematische modellen voor programma’s kunnen ontwerpers informatie geven over de bedrijfszekerheid ervan.
‘Om zekerheid te krijgen over het gedrag van een programma moet het worden geanalyseerd. Dit kan bijvoorbeeld door een model van het programma te maken en de gewenste eigenschap in termen van dit model te vertalen. Daarna kan een eigenschap bewezen worden door te bewijzen dat de vertaling ervan binnen het model geldt. Bij het wiskundig modelleren van een programma is een eigenschap met wiskundige zekerheid te bewijzen’, aldus Arts.
In het recente verleden ontwikkelde termherschrijfsystemen zijn geschikt gebleken om computerprogramma’s te modelleren. Nadat een model is opgesteld, kan aangetoond worden dat het programma over bepaalde eigenschappen beschikt door eigenschappen van het modellerend termherschrijfsysteem te bewijzen. Dat komt overeen met wat een astronoom doet die met een wiskundig model bewijst dat de zwaartekracht op Jupiter groter is dan op aarde.
Vastlopen
In zijn proefschrift behandelt Arts twee eigenschappen van termherschrijfsystemen: terminatie (vastlopen) en innermost normalisatie (een variant op vastlopen). Dat zijn twee eigenschappen die een softwareprogramma kan hebben.
Twee eigenschappen lijkt weinig, maar een proefschrift kan niet alle mogelijke eigenschappen van een termherschrijfsysteem en daarmee van een softwareprogramma behandelen. Door wiskundig te bewijzen dat een termherschrijfsysteem over de eigenschap ’terminatie’ beschikt, bewijst Arts dat een met zo’n systeem beschreven programma werkelijk niet zal blijven hangen in oneindige lussen (termineert). De methode is daardoor nu al toepasbaar voor het testen van softwaresystemen op de eigenschap ‘vastlopen’.
Arts: "Hangende computerprogramma’s behoren met dit onderzoek tot de verleden tijd. Ik kan nu bijvoorbeeld voor verschillende programma’s bewijzen dat een computer niet blijft ‘hangen’ als hij programma’s uitvoert. Ook andere gewenste eigenschappen van een programma zijn aan te tonen door te bewijzen dat een bepaald termherschrijfsysteem termineert. Het is bijvoorbeeld mogelijk om een bewijs dat een termherschrijfsysteem termineert te gebruiken om aan te tonen dat de uitkomst van een door het gemodelleerde programma uitgevoerde berekening uniek is."
Doorbraak
Daarmee geeft Arts aan dat zijn onderzoek verder gaat dan het aantonen van de eigenschap ‘vastlopen’ in softwaresystemen. Hoewel het proefschrift alleen terminatie en innermost normalisatie behandelt, heeft het als bredere waarde dat de IT-branche nu over een techniek beschikt waarmee in principe alle eigenschappen van programma’s automatisch zijn aan te tonen. Dankzij Arts’ werk kan in de toekomst een computerprogramma de ontwikkelaar gaan helpen om software te testen. Daarmee lijkt op langere termijn een eind te kunnen komen aan de hegemonie van de niet altijd betrouwbare testmethodes. Voor de IT is dat een innovatieve doorbraak.
Vooral het aantonen van de eigenschap ‘innermost normalisatie’ is voor de IT-branche van belang. Technieken om terminatie automatisch te bewijzen bestonden namelijk al. Arts toont aan dat ook innermost normalisatie automatisch te bewijzen valt.
"Het blijkt mogelijk om voor een grote groep termherschrijfsystemen terminatie te bewijzen via de techniek waarmee innermost normalisatie te bewijzen is. Door de logische programma’s te vertalen naar termherschrijfsystemen en vervolgens van die systemen innermost normalisatie te bewijzen, valt ook terminatie van logische programma’s te bewijzen", zegt Arts.
