Holzmann - baard, bril, polo, spijkerbroek, vriendelijke blik, tikkeltje verlegen maar een boeiende verteller, zo blijkt - is `buitengewoon' vereerd met het eredoctoraat dat hij vrijdag 1 december krijgt uitgereikt. `Vooral omdat het een Nederlandse universiteit betreft.'
De UT prijst uw rol in de informatica en de impact van uw vinding - de SPIN model checker - voor het vakgebied. Wat vindt u daarvan?
`Ik heb geluk dat ik in het juiste vakgebied werk. Daarin is de correctheid van software het belangrijkste `open' probleem. Wat ik wil bereiken is moeilijk en uitdagend. Het gaat steeds om kleine stapjes. Als je die bij elkaar optelt, zijn het inderdaad belangrijke ontwikkelingen, zoals SPIN. Vele tienduizenden mensen op de wereld gebruiken dat model. Daarmee halen ze fouten uit hun software. Het gaat vaak om kritische toepassingen. Ik krijg dagelijks tientallen mailtjes van gebruikers die me bedanken. Ik beantwoord ze allemaal. Het geeft een goed gevoel dat mensen er profijt van hebben. Het kostte me twintig jaar, maar ik kreeg het voor elkaar. Maar eerlijk is eerlijk, ik had SPIN niet kunnen ontwikkelen in een andere omgeving dan bij Bell Labs, mijn vorige werkgever. Of althans, dan had het veel langer geduurd.'
Holzmann's loopbaan staat in het teken van zijn werk bij het wereldberoemde Bell Labs in Murray Hill, New Jersey aan de Amerikaanse oostkust, waar hij 23 jaar werkte. Hoe hij daar in 1980 binnenkwam, is een verhaal apart. Als postdoc op een Fulbrightbeurs had hij er, na zijn promotie in Delft, al een tijdje gezeten, maar toen zijn beurs was verstreken moest hij weer naar Nederland. `De volgende logische loopbaanstap zou Carnegie Mellon zijn geweest en daarna MIT. Of Harvard, of Stanford. Maar dat wilde ik niet! Ik was zo bezeten van Bell Labs dat ik besloot om mijn toekomst daarop te richten.'
Dus schreef de jonge, begaafde Holzmann, nog geen dertig, in 1980 een sollicitatiebrief naar het instituut van zijn dromen. Op hoop van zegen. `Ik dacht: de kans dat ik binnenkom is nul komma nul. En ja hoor, ik had een verkeerde contactpersoon doorgekregen en die vent had m'n brief gemakshalve maar doorgestuurd naar personeelszaken. En die krijgen daar honderden van die brieven, die dan weer verdeeld worden over de afdelingen. Blijkt het hoofd van computing research (waar ik wilde werken) mijn brief er toch uit te hebben gepikt. Simpel en alleen omdat hij de naam had herkend van mijn promotie-supervisor in Nederland, professor Van der Poel. Die is nu in de tachtig en ik verwacht hem bij de uitreiking in Twente. Van der Poel was de man die de eerste computer in Nederland bouwde, in de vijftiger jaren. Dus dacht Doug (het afdelingshoofd): `het minste wat ik kan doen is die Nederlandse professor om een aanbeveling vragen.'
Nou was er in die tijd noch email noch een andere snelle verbinding. Van der Poel schreef een aanbeveling van één paragraafje. Holzmann: `Zijn secretaresse meende er verstandig aan te doen om die voor mij zo belangrijke aanbeveling niet per luchtpost te versturen, maar per boot. En dat duurde zes weken. Dus die Doug hoorde maar niks en besloot na twee weken mijn naam te schrappen. Ik kreeg een brief met bedankt voor de moeite en good luck in your career. Ik baalde als een stier. Maar wat gebeurt er: na zes weken komt die brief uit Nederland alsnog binnen bij Bell Labs, op het goede adres, bij Doug dus. En die ene paragraaf was voor hem voldoende om mij direct per telegram te vragen of ik nog beschikbaar was. Ik blij natuurlijk.'
Het was het begin van een glanzende, opwindende tijd bij het topinstituut aan de Amerikaanse oostkust. Hij werkte er jarenlang aan wat je zijn levenswerk zou kunnen noemen: de creatie en vervolmaking van de SPIN model checker, het onder informatici vertrouwde softwarepakket voor het ontdekken van fouten in software. Holzmann kreeg er in april 2002 de prestigieuze Software System Award van de Amerikaanse Association for Computing Machinery voor. Zijn creatie werd aanvankelijk ingezet voor het testen van complexe switching-systemen voor telefooncentrales. Al snel bleek het pakket zich echter ook te lenen voor het controleren van fouten in andere applicaties, waaronder IP-applicaties, treinverkeerssystemen, besturingssystemen voor kerncentrales en toepassingen voor de ruimtevaart. De NASA gebruikt SPIN sinds de problemen met de Mars Pathfinder-missie. Want die hadden voorkomen kunnen worden door de software beter te testen. Holzmann was de derde Bell Labs-medewerker die de Software System Award won. Eerder werden Ken Thompson en Dennis Ritchie, de ontwikkelaars van UNIX, en John M. Chambers, die het S System ontwikkelde, onderscheiden met deze prijs.
Bell Labs dus. Het laboratorium met zo ongeveer het hoogste IQ ter wereld maakte eind jaren zeventig, begin jaren tachtig deel uit van AT&T. Holzmann: `AT&T was destijds een van de grootste en rijkste ondernemingen ter wereld sinds ze het telefoonnet van Amerika gingen exploiteren. Voor onderzoekers groeiden de bomen tot in de hemel. Wat een kennis en talent zat er in de reserarchlabs. Ik werkte er temidden van een Nobelprijswinnaar en andere topwetenschappers in de fysica, wiskunde en computerscience. De groep waar ik zat was verantwoordelijk voor UNIX en de ontwikkeling van de programmeertalen C en C++. De ambiance was fantastisch, dat vond je nergens. Ja, de selectie was heel streng, maar eenmaal binnen had je complete vrijheid in waar je aan wilde werken en hoe lang. Er waren geen grenzen. Alle facetten van de wetenschap werden bestreken. In zo'n omgeving was het niet zo moeilijk om te floreren. The big attraction was: no requirement at all to refunding proposals and no meetings. Je hoefde aan niemand te vertellen waar je mee bezig was of waarom. Only science, pure science. Het enige wat er ieder jaar van je gevraagd werd was om op één paginaatje A4 uit te leggen wat je dat jaar had gedaan.'
De jaren tachtig en de vroege negentig bij Bell Labs waren super, met fantastische mensen en onuitputtelijke bronnen, aldus Holzmann. Hij begon er als lid van de technische staf en kreeg pas later een leidinggevende functie. `Met veel vergaderingen en beheersmatige zaken. Dat veranderde mijn rol als wetenschapper.'
Langzaam maar zeker zag hij AT&T wankelen: bedrijfsonderdelen werden afgestoten, in 1996 scheidde Lucent Technologies zich af en in 2001 -na de beurskrach- zakte het aandeel naar een absoluut dieptepunt. `Het was fascinerend om te zien hoe dat enorme, dominante bedrijf dat een monopolie bezat in Amerika, voor je ogen veranderde van een supermacht tot een veel kleinere speler, met name na 2001. Mensen vertrokken, het talent droogde op, onderzoeksprojecten werden gestopt.'
Wat was de oorzaak van die ineenstorting? Verkeerd management?
`Marktwerking, concurrentie. AT&T hield zich daar niet staande in.'
Was die absolute vrijheid van wetenschapsbeoefening zonder enige verplichte verantwoording daar wellicht ook debet aan?
`Nee. Integendeel, die vrijheid was in het bestaan van Bell Labs altijd een succesfactor geweest. Alle grote uitvindingen van de twintigste eeuw kwamen uit Bell Labs. De transistor, de CCD, de laser, het unix operating system, de main programming languages, alle uitvindingen in de computerscience, noem ze maar op. Maar het was een commercieel bedrijf, net als bijvoorbeeld Philips. Dat kon zich op een gegeven moment ook niet meer veroorloven om fundamentele research te doen zonder koppeling met producten.'
Langzaam maar zeker raakte Holzmann's groep compleet uitgedund. `Ik was zo ongeveer de laatste der Mohicanen.' Hij was destijds leider van `computing principles research', een groep van dertig mensen. `We werkten honderd uur per week. Niemand vertelde ons om naar huis te gaan of zo. Ik stond op, werkte, sliep en begon in mijn slaap al problemen op te lossen. Dat heb ik een hele tijd gedaan. De uitdaging van het werk slurpte je op, het liet je niet meer los. Je wilde oplossen waar je mee bezig was, je stopte niet om vijf uur, je ging door tot het bittere eind. Ik denk daar trouwens nog steeds zo over. Het was een buitengewone tijd, maar er kwam een eind aan.'
In 2003 vertrok Holzmann bij Bell Labs na een, in wetenschappelijk opzicht, hele vruchtbare periode. En ook toen gebeurde er iets wonderlijks.
Holzmann: `Het bedrijf hield uitverkoop van zijn personeel. Ze boden de meest productieve mensen - de laatveertigers, beginvijftigers zoals ik- een vertrekpremie aan. Ik sloeg dat aanbod af. Vertrekken kon immers later ook nog wel, gokte ik. Maar ik dacht natuurlijk wel na over een andere baan. Er waren drie opties: Microsoft, Google en JPL. Ze wilden me alle drie wel, maar JPL trok het hardste aan me. Ze boden me uitdaging en perspectief. Ik kon mijn voorwaarden stellen, dat was voor mij op dat moment belangrijker dan het feit dat ik bij Google een flink aandelenpakket had kunnen krijgen, net als al mijn really smart collegues. Je raadt al wat er gebeurde: de Google-aandelen kwamen op de beurs en dat leverde mijn ex-collega's stuk voor stuk twintig miljoen dollar op. Twintig miljoen, die liep ik dus mis!
`Ik had aan de ene kant spijt, natuurlijk, maar anderzijds zijn de toepassingen bij JPL veel en veel interessanter dan bij Google. Dat telt voor mij. Bij Google gaat het allemaal wat sneller, maar ik kan met trots zeggen: dat ding is zojuist geland op Mars. Dat is het verschil.'
Holzmann werkt nu drieëneenhalf jaar bij JPL, een omgeving die veel weg heeft van wat hij bij Bell Labs in het begin meemaakte. Ruimte voor goed onderzoek, veel faciliteiten, slimme, gepassioneerde wetenschappers die niet praten over koetjes en kalfjes, maar over wetenschap en ruimtevaartonderzoek. `Het gaat om de software die het apparaat de ruimte in stuurt. We zitten er als het ware bovenop. Wat we in principe doen, is betere methoden ontwikkkelen om de door deskundigen aangeleverde software te controleren op fouten. De uitdaging is om stukjes software te schrijven met de mathematische zekerheid dat ze niet zullen falen.'
De geboren Amsterdammer karakteriseert zich als een `typische vogel'. `Mijn omgeving zal dat bevestigen. Een van mijn hebbelijkheden is dat ik niet van regels hou, want rules never make sense. Ja, ik ben tegendraads, trek m'n eigen plan.' Lacht. `Wat dat betreft is het een mirakel dat ik nog getrouwd ben. Regels zijn vaak zo dubbel en voor meerdere uitleg vatbaar. Dat geeft alleen maar verwarring. Logica en wiskunde, grote nauwkeurigheid, dat heb ik allemaal nodig in mijn werk. Je moet er voor zorgen dat de computer doet wat jij wilt, want het is een dom ding. Er is geen ruimte voor dubbelzinnigheid. Een hoop mensen zullen daarom wel een hekel aan me hebben.'
Alhoewel, zijn bazen, voorzover je daar van kan spreken, zien die eigenschappen gelukkig als een kwaliteit die je nodig hebt om in deze rol goed te functioneren, bevestigt hij. `Ik ontdek de zwakheid van een ontwerp, waar anderen overheen kijken. Ik bouw een team om me heen van gelijkgestemde, nauwkeurige en eigenwijze mensen. Dat boeit me'.
Een ander aspect van zijn loopbaan betreft de portretfotografie, tevens zijn grote hobby. `Ik heb thuis een hele professionele studio. Bekijk mijn website. Bij Bells kon ik ook ongestoord werken aan digitale fotografie, lang voor die apparaten op de markt kwamen. Een digitale camera was toen al te bouwen, maar ik stuitte bij de hardwaremensen op een muur van verzet: ze beweerden dat het apparaat veel te groot zou worden. Veel van de dingen die ik toen ontwikkelde vind je nu terug in Photoshop en andere programma's. Nee, rijk ben ik niet geworden van die acht of negen patenten. Bell Labs houdt ze in stand: het kost me niks maar het levert ook niks op.'
Enig idee hoe de pc van de toekomst eruit ziet?
Holzmann: `Nee. Dat is nou precies de enige reden waarom ik zo lang mogelijk wil leven: om te zien waar dit heen gaat. Het is toch fenomenaal was er in de laatste vijfentwintig jaar is gebeurd. Just astonishing! Kijk naar de computers waar ik eerst aan werkte en die van nu, qua snelheid en geheugen. Je kon tot voor kort iedere twee jaar een machine kopen die twee keer zo snel was als de vorige, met twee keer zoveel geheugen. Dat was revolutionair. De impact was enorm. En nog steeds. Het maakt dingen mogelijk en betaalbaar die onmogelijk en onvoorstelbaar werden geacht. Ik zou zo graag willen weten hoe de zaken er over vijftig jaar voorstaan. Wat kunnen we dan allemaal wel niet?'
Vertaalslag
Holzmann is voorgedragen door Ed Brinksma (1957), gepromoveerd aan de UT en sinds zijn benoeming in Eindhoven deeltijdhoogleraar aan de UT bij de leerstoel Formal Methods and Tools. In de lichtstad is hij sinds anderhalf jaar wetenschappelijk directeur en directievoorzitter van het Embedded Systems Institute. Brinksma ontmoette Holzmann begin jaren tachtig tijdens een conferentie in de VS. Ze waren beiden bezig met de modellering van communicatiesoftware. De twee hielden contact, maar van gezamenlijke projecten kwam het niet. `Holzmann is een wetenschapper die het liefst in z'n eentje het werk verzet. Ook de SPIN model checker heeft-ie zelf gemaakt.'
Brinksma noemt de SPIN van Holzmann een `ongelofelijke kwaliteitsverbetering'. Legt uit: `Programmatuur van computers is zeer complex. Het is onvermijdelijk dat daar fouten in komen. Software komt tegenwoordig overal in voor. We worden steeds afhankelijker van de betrouwbaarheid daarvan, maar die betrouwbaarheid is niet altijd in orde. Een model checker checkt zo nauwkeurig mogelijk of het systeem niet in een andere toestand verkeert dan de wenselijke. Denk maar aan het bouwen van een brug. Eerst maak je de berekeningen: wat kan-ie dragen, hoe groot en zwaar mag-ie zijn en welk materiaal gebruik je. Dan maak je een model. En dat moet kloppen.'
Brinksma noemt zijn collega een pionier. `Het theoretische idee van model checking komt uit de wiskundige logica. Holzmann heeft de vertaalslag gemaakt naar bruikbare resultaten, door er vele jaren onderzoek in te steken en te praten met gebruikers.'
Boeken en full text artikelen zijn te vinden op op www.utwente.nl/ub/news
Volgende week: reportage over Stanford University, de nummer twee van de wereld (waar meerdere ex-UT-studenten werken), plus een artikel over Sung Wan Kim (1940), hoogleraar aan de University of Utah in Salt Lake City, aan wie de UT ook een eredoctoraat heeft toegekend. Vorige edities: portretten van de laureaten Fraser Stoddart (UCLA) en Sheila Jasanoff (Harvard).
Center of excellence
De Maanlander, die in levende lijve staat opgesteld in het Jet Propulsion Laboratory in Pasadena, trekt jaarlijks vele schoolklassen die met eigen ogen kunnen bekijken hoe het futuristische voertuig er in het echt uitziet. Verderop in het hoofdgebouw staan allerlei andere ruimtevaartattributen, apparatuur en fotodecors van eerdere NASA-missies die sinds het begin van het ruimtevaart tijdperk (met de lancering van de Explorer 1 op 31 januari 1958) werden uitgevoerd. De Explorer werd door het JPL gebouwd. Sindsdien heeft het instituut onbemande missies verzorgd naar elke planeet van het zonnestelsel, op Pluto na. JPL beheert ook het wereldwijde Deep Space Network, gevestigd in de Mojave Woestijn van Californië, Madrid en Canberra.
Het laboratorium valt onder beheer van het California Institute of Technology (Caltech), eveneens onder de rook van Los Angeles. Holzmann is net als zijn andere collega's dus werknemer van Caltech, dat met z'n slechts 2100 studenten tot de toptien van de wereld wordt gerekend (net als MIT in Boston). JPL is een autonoom operend ruimtevaartcentrum dat langlopend contractonderzoek uitvoert voor NASA, wat staat voor National Aeronautics and Space Administration.
Er werken meer dan vijfduizend mensen op het enorme JPL-complex, waar ook de apparatuur wordt gebouwd en de vluchten worden begeleid. Holzmann is binnen JPL het hoofd van het ongeveer dertig wetenschappers tellende center of excellence LaRS, het onderzoekscentrum voor `reliable software'. `Het gaat om de software die ervoor zorgt dat het apparaat de ruimte in wordt geschoten en in het heelal zijn opdrachten uitvoert. We zitten dus inderdaad heel dicht tegen het spektakel aan.' De van de TV-journaals bekende zaal waar de vluchtleiding een ruimtevaartmissie volgt is vanachter glas te zien. Ook Gerard Holzmann is er op hoogtijdagen te vinden. De leek die denkt dat het ruimtewagentje direct, met een druk op de knop, vanaf JPL is aan te sturen, komt bedrogen uit. `Een opdracht vanaf de grond doet er twintig minuten over om het apparaat te bereiken. Dat schiet dus niet op. Als we willen dat het ding een bocht naar links of rechts maakt of een andere dan de voorgeprogrammeerde handeling verricht, schrijven we daar speciale software voor. En dan zien we de andere dag wel of het allemaal heeft gewerkt, aldus Holzmann die vertelt dat er tijdens de lancering, om te spanning te relativeren, nootjes (`peanuts') worden uitgereikt. Holzmann roemt het `JPL-gevoel', een soort `vaderlandsliefde'. `Er zitten hier louter gepassioneerde wetenschappers met hart voor hun werk.' Geld voor onderzoek is er voldoende, `maar vraag me niet of ik het geldverdeelmodel kan volgen. Dat blijft een mysterie.'
Bekende projecten zijn de Galileo Jupiter missie en de Mars Rovers, zoals de Mars Pathfinder (1997) en de Mars Exploration Rovers (in 2003).
