Veilig landen op Mars

Op 1 december kreeg NASA-informaticus dr. Gerard Holzmann een eredoctoraat uitgereikt door de Universiteit Twente voor zijn pionierswerk op het gebied van betrouwbare software. Een interview.

Wereldwijd maken tienduizenden mensen gebruik van SPIN om de betrouwbaarheid van hun software te controleren. Wat is de kracht van SPIN?

“Veel kritische toepassingen – voor bijvoorbeeld de besturing van telefooncentrales en ruimtevaartuigen – bestaan tegenwoordig uit multithreaded systemen. Dat soort systemen zijn zo complex dat je hun betrouwbaarheid niet kunt garanderen door te testen of ze nauwkeurig te bestuderen. Je hebt dus een ander soort gereedschap nodig, zoals SPIN. De grote kracht van SPIN is dat programmeurs alle theorie die erin verwerkt is niet hoeven te kennen om de tool toch te kunnen gebruiken.”

Hoe werkt SPIN?

“SPIN bouwt een model van een programma. Daarin wordt heel precies vastgelegd wat de software doet op een formeel niveau. In multithreaded systemen gaat het altijd om grote aantallen processen, die tegelijkertijd werkzaam zijn. Ze hebben toegang tot gemeenschappelijke bronnen en kunnen elkaar dus in de weg lopen. Het formaliseren van al het mogelijke gedrag van de software is stap één. Stap twee is om vast te leggen welke eigenschappen de software moet hebben om correct te zijn. Eén van die eigenschappen is meestal dat het systeem niet in een deadlock terecht mag komen. Een andere eigenschap kan bijvoorbeeld zijn dat er geen leader election-probleem mag optreden – dus het algoritme dat ervoor zorgt dat één proces uiteindelijk de controle over het hele systeem uitvoert moet exact één leider opleveren. Zo’n eigenschap formaliseer je ook. Je beschrijft dat er niet minder dan één, en ook niet meer dan één leider mag opstaan, en dat de keuze binnen een eindige tijd gemaakt is. Dan heb je twee verschillende formalisaties van je software. Die twee formalisaties moeten logisch en consistent met elkaar zijn. SPIN controleert of dat ook echt zo is. De tool zoekt naar systeemgedrag waarbij er een conflict optreedt tussen die twee eigenschappen.”

Onder welke omstandigheden hebt u SPIN ontwikkeld?

“Na mijn promotie in 1979 aan de Technische Universiteit in Delft kwam ik bij Bell Labs terecht. Ze vroegen me daar om een correctheidsbewijs te geven van een stuk software voor het besturen van een telefooncentrale. Ik wist niet hoe je dat moest doen en zij wisten het ook niet. Het kostte me zo’n vijftien jaar om een tool te ontwikkelen die dat kon oplossen. Die tool werd uiteindelijk SPIN. Het is dus een heel langdurig proces geweest.”

Waarom was het zo moeilijk?

“Omdat het heel moeilijk is om de correctheid van software met honderd procent zekerheid te bewijzen, om een garantie te kunnen geven dat het correct zal werken, onder alle omstandigheden.”

Op welke toepassingen van SPIN bent u het meest trots?

“Er zijn er een paar. Zoals het controleren van de stormvloedkering bij Rotterdam, wat de Universiteit Twente zo’n tien jaar geleden heeft gedaan. Voor een oud-Nederlander is dat natuurlijk een hele leuke toepassing. En het is een toepassing die ik ook aan mijn moeder kan uitleggen. Het is altijd heel moeilijk om aan je ouders uit te leggen waar je aan werkt. Andere hele belangrijke toepassingen zijn voor de NASA.”

Zijn er al ruimtevaartsuccessen aan u te danken?

“Op die manier werkt het niet. Je kunt nooit zeggen: deze missie is geslaagd omdat wij een fout uit het systeem gehaald hebben. Een voorbeeld is de Cassini-missie, het ruimtevaartuig dat nu om Saturnus heen cirkelt. Voordat die gelanceerd werd in 1997 hebben we het besturingssyteem gecontroleerd met SPIN. We hebben toen drie belangrijke fouten uit het beschermingssysteem gehaald. Voor de veiligheid zijn er twee exact gelijke computers voor de besturing. Als de één in de problemen komt, dan schakelt het systeem over naar de tweede. De fouten die wij vonden hadden te maken met de correctheid van de overschakeling van de ene naar de andere computer. Er zijn tijdens de vlucht van de Cassini tot nu toe zeker drie momenten geweest waarop is overgeschakeld naar de tweede computer. Als die fouten er niet uit waren gehaald, was er een kans geweest dat Cassini op die momenten onbestuurbaar was geworden. Maar bij dat soort complexe systemen weet je nooit honderd procent zeker of dat ook daadwerkelijk was gebeurd. Maar wij hebben in ieder geval uitgesloten dat het kan gebeuren en daarmee de software betrouwbaarder gemaakt.”

Waar werkt u nu aan?

“Aan de software voor de volgende landing op Mars in 2010. De lancering daarvoor is in 2009. We zijn er vooral op gespitst om het systeem voor bestandsbeheer heel robuust te maken, zodat de communicatie met de aarde nooit faalt, waardoor je foto’s en andere data zou kunnen verliezen.”

Wat vindt u ervan dat onze wereld steeds afhankelijker wordt van computers?

“Dat brengt natuurlijk gevaren met zich mee, maar ik denk dat de baten veel groter zijn dan de risico’s.”

Vindt u dat computersystemen voldoende worden gecontroleerd op betrouwbaarheid?

“Absoluut niet. Gereedschappen zoals SPIN worden wel steeds meer gebruikt. Binnen de NASA is het ondenkbaar om dat niet te doen. Ook veel andere bedrijven, zoals Microsoft, gebruiken SPIN en ontwikkelen zelf vergelijkbare tools.”

Kunt u voorbeelden noemen van systemen die onvoldoende worden gecontroleerd?

“Ik zaai liever geen paniek, maar in elke auto zijn tegenwoordig verschillende processoren ingebed. In principe is de hele besturing van de auto geautomatiseerd. Dat geldt voor de remmen, maar ook voor bijvoorbeeld de besturing van de wielen. De software daarvoor wordt meestal in C geschreven. Die code wordt tegenwoordig nog onvoldoende gecontroleerd. Dat kan uiteindelijk tot consequenties leiden. Als die software faalt, kunnen er echt hele vervelende dingen gebeuren.”

Hebt u nog meer voorbeelden?

“Ook standaard desktoptoepassingen zoals het Windows-besturingssysteem worden nog onvoldoende gecontroleerd. Windows bevat twintig tot dertig miljoen regels programmatekst. Dat is veel te veel voor de geleverde functionaliteit. Hoe groter een programma, hoe minder betrouwbaar en hoe moeilijker testbaar. Dat besef moet echt nog doordringen.”

Eigenlijk pleit u ervoor om Windows helemaal van de grond af opnieuw te ontwerpen?

“Ja. En als Microsoft het niet doet, zijn er wel andere bedrijven die dat doen. De markt zal vervolgens bepalen welk bedrijf uiteindelijk wint. Tot nu toe heeft Microsoft een groot monopolie op het gebied van besturingssystemen. Maar in de komende vijf jaar zullen er startups opstaan die garantie geven op de correctheid en betrouwbaarheid van hun besturingssysteem. Die zullen zeggen: als mijn systeem faalt, krijg jij je geld terug. En als je financiële schade lijdt, dan sta ik daarvoor ook garant.”

Dat zou revolutionair zijn.

“Ja, maar ik denk dat dit zeker zal gebeuren.”

Daar is een hele grote markt voor.

“Absoluut. Stel je voor dat de computers op Wall Street down gaan. Dan kost dat miljarden dollars. Maar ook gewone consumenten zijn erbij gebaat. En bedrijven. Als de computers bij jouw bedrijf een hele dag niet werken, dan kost dat erg veel geld.”

Bij Bell Labs had u heel veel vrijheid om aan uw ideeën te werken. Want vindt u van het huidige klimaat voor wetenschappers?

“De wereld verandert. Het klimaat zoals het bij Bell Labs bestond, was ook in de tachtiger en negentiger jaren al uitzonderlijk. Zoiets kan in feite alleen bestaan bij een heel groot bedrijf, zoals AT&T, dat toentertijd een monopolie had op telefonie in Amerika. Die kon zich dat veroorloven, maar het is eigenlijk niet realistisch om te verwachten dat je als informaticaonderzoeker in zo’n omgeving terecht komt. Er zijn echter nog steeds bedrijven waar je heel goed onderzoek kunt doen. Je kunt er weliswaar met wat minder vrijheid, maar toch zeker aan interessante problemen werken. Google is daarvan een voorbeeld, maar ook Microsoft heeft een hele sterke onderzoeksorganisatie. Bij NASA bestaat vanzelfsprekend zeer veel belangstelling voor de betrouwbaarheid van software. En de Universiteit Twente herbergt een van de beste onderzoeksgroepen op dat gebied wereldwijd.

Maar het klopt dat wetenschappers zich tegenwoordig sterker moeten verantwoorden. Er is minder vertrouwen dat als je iemand gewoon loslaat hij uiteindelijk wel met iets gaat komen. Bij Bell Labs heeft dat heel goed gewerkt. Er zijn hele belangrijke uitvindingen uit dat lab gekomen. Zoals de transistor, de laser, de CCD (de charge-coupled device, die tegenwoordig in elke digitale camera zit), noem maar op. Dat had waarschijnlijk niet in een andere omgeving kunnen gebeuren.”