Uitgesproken op 5 maart 1999 aan de Technische Universiteit Eindhoven

Mijnheer de Rector Magnificus, dames en heren.

De informatica is een ingenieursdiscipline met een heel eigen karakteristiek. Ze bestudeert discrete dynamische systemen die buitengewoon flexibel zijn, en die meestal met de term computer worden aangeduid. De flexibiliteit staat het toe in relatief korte tijd en met relatief weinig moeite systemen te bouwen die zeer complexe taken met hoge snelheid en grote precisie kunnen uitvoeren.

Hierdoor heeft de computer een grote invloed op ons dagelijks leven. Vele arbeidsintensieve taken blijken uitstekend door computers te kunnen worden uitgevoerd. Deze worden niet alleen gevonden in het financiële verkeer of bij productieprocessen, maar ze betreffen bijvoorbeeld ook zorgtaken in ziekenhuizen. Dit heeft ons extra welvaart gebracht zonder de omvangrijke problemen te veroorzaken die bijvoorbeeld de industriële revolutie met zich meebracht.

Vanwege de enorme economische voordelen zijn computers overal grootschalig en haastig ingevoerd. Nu, na ongeveer 40 jaar automatisering, spreekt men over het legacy probleem. Bedrijven zijn afhankelijk geworden van software van gigantische omvang die niemand beheerst. Dit betreft niet alleen banken of pensioenfondsen, maar ook ontwikkelaars van softwaregestuurde apparaten, zoals telefooncentrales. In dit licht bezien is het millennium probleem slechts een onderdeel van een veel fundamenteler vraagstuk: wanneer en waarom functioneert de software niet zoals verwacht. Het millennium probleem heeft als typisch aspect dat het zich op één moment zou kunnen manifesteren, waarbij de samenleving wat meer moeite heeft het probleem op te vangen. Maar feitelijk wordt er al continu veel energie gestoken in het ondersteunen van systemen die niet helemaal functioneren zoals bedoeld.

Door het grootschalige gebruik van computers is er aan anekdotes over wat er mis kan gaan geen gebrek. Recentelijk zijn er twee grote deuren in de Nieuwe Waterweg gebouwd om bij gevaarlijke springvloed Rotterdam te beschermen. De deuren hoeven waarschijnlijk slechts eens in de 10 jaar te sluiten. Omdat de deuren zo weinig sluiten, is het psychologisch onverantwoord het sluiten aan een mens over te laten. Er is een computer die beslist wanneer de deuren dicht gaan, en er zijn computers die er voor zorg dragen dat de deuren sluiten. Hiertussen zit een computernetwerk waarover de beslissing om te sluiten wordt gecommuniceerd. De wijze waarop deze communicatie plaats vindt heet een protocol. De makers van het beslissysteem vermoedden dat dit protocol niet goed functioneerde. Bij het sluiten kon het protocol in een deadlock raken, waarna het niet mogelijk zou zijn de deuren op de normale manier te openen. Met moderne analysehulpmiddelen kon dit vermoeden worden bevestigd. Op dit moment is het protocol vervangen door een verbeterde, en gevalideerde versie, en is de kans vergroot dat de deuren goed zullen blijken te werken.

Dit is een positief voorbeeld van een probleem in een programma. Het probleem is gedetecteerd en verholpen, voordat het enige serieuze consequentie had. Van het verbeterde protocol is bewezen dat het goed functioneert. Zorgwekkend is het om te zien hoeveel moeite het kostte iedereen te overtuigen van het bestaan van het probleem. Het is één van de vele signalen dat de complexiteit van computers nog systematisch wordt onderschat. Zorgwekkend is ook dat het hier slechts een fractie van het totale systeem betreft. Hoewel de software in het systeem met de grootste zorgvuldigheid is geconstrueerd, wordt dit onderdeel als de zwakste schakel van de waterkering in de Nieuwe Waterweg gezien, terwijl de software minder dan een procent van het hele systeem heeft gekost.

Het bovenstaande voorbeeld is ook een van de vele signalen dat de behoefte groeiende is software beter te beheersen. Hiervoor zijn een aantal redenen.

Computergestuurde systemen zullen nog veel ingewikkelder worden dan ze nu zijn. Ze zullen op steeds meer taken worden ingezet, waarbij steeds meer verantwoordelijkheden aan computers zullen worden toevertrouwd. In Parijs is een nieuwe metrolijn gebouwd waarop de metrobestuurder is afgeschaft, opdat de treinen dichter op elkaar kunnen rijden. De Nederlandse Spoorwegen overwegen om het hele seinstelsel in Nederland te vervangen door een ander aanzienlijk complexer besturingssysteem om de capaciteit van de spoorbanen te vergroten.

Ik juich bovenstaande ontwikkelingen van harte toe. Bij goed gebruik biedt het immers de mogelijkheid onze samenleving tot een nog aangenamere te maken.

Maar de huidige ontwikkeling heeft ook negatieve kanten. Zonder structurele verandering van het softwareproductieproces zal de toenemende autonomie en complexiteit van computersystemen tot steeds meer ongelukken aanleiding geven. Opnieuw een voorbeeld als een voorteken daarvan.

Bij Eurocontrol in Brussel worden de protocollen voor de communicatie tussen vliegtuigen gedefinieerd. Het idee is dat ergens in het komende decennium het overgrote deel van de communicatie per computer verloopt, en dat de piloot slechts ingrijpt in het geval van een probleem. Bij analyse van de eenvoudigste van deze protocollen, bleken ze al niet noodzakelijkerwijs goed te functioneren. Het betrof een protocol, dat wordt gebruikt wanneer twee vliegtuigen recht op elkaar af vliegen. De bedoeling is dat wordt afgesproken wie omhoog vliegt, en wie omlaag, zodat een botsing wordt vermeden. Aangetoond kon worden dat de symmetrie niet gegarandeerd werd verbroken. Bij mijn weten was de analyse van dit protocol een geïsoleerde activiteit, en zijn de ingewikkelder protocollen nooit aan een dergelijke analyse onderworpen.

Er is nog een reden waarom beheersing van software belangrijker wordt. Gebruikers van software zullen in de komende jaren betrouwbaarheid van software veel zwaarder laten wegen. De functionaliteit van veel softwarepakketten nam in de afgelopen jaren met een snel tempo toe, waarbij de aanschafprijs stabiel bleef. In zo’n situatie verkoopt software met extra functionaliteit het best en wordt aan betrouwbaarheid of bruikbaarheid minder aandacht geschonken. Volgens opgaaf van Microsoft bevatte Windows 95 minimaal 5000 fouten. Velen ervaren deze fouten dagelijks. Desondanks is Windows 95 een doorslaand succes geworden.

Maar de functionaliteit van veel softwarepaketten stabiliseert. Nieuwe versies verschillen maar matig van hun voorgangers. Softwareproducenten zullen de kwaliteit van de programma’s moeten verbeteren om concurrerend te blijven. Dat betekent dat ze meer aandacht zullen moeten besteden aan het correct functioneren van de software.

Waarom treden er zo vaak problemen met software op? Software wordt in grote lijnen nog steeds op dezelfde manier gemaakt als 30 jaar geleden. Er is wel iets veranderd. Nu gebruiken we moderne programmeertalen, onvergelijkbaar snellere computers, superieure compilers en debuggers, en is er veel meer aandacht voor het softwareontwerpproces, met uitgebreide documentatie, testen en peer review. Hierdoor is de kwaliteit van de code ontegenzeglijk verbeterd, maar er zijn nog vele zwakke schakels.

Software wordt over het algemeen vanuit vage doelstellingen geconstrueerd. Vaak worden de beoogde taken van de software in natuurlijke taal gevat, en wordt daarbij ook een schets van een mogelijke implementatie gegeven, die meestal bedoeld is om de werking te definiëren. Een typische verwarring die hierdoor ontstaat is dat het niet duidelijk is wat een harde eis is, en wat een suggestieve toelichting.

Er zijn veel methoden om het ontwerpproces te assisteren. Meestal richten deze methoden zich op enkele statische aspecten, zoals de structurering van de datatypes of de implementatiearchitectuur. Vaak werken de methoden met voorbeelden, bijvoorbeeld in de vorm van message sequence charts. De definiërende kracht van deze methoden is beperkt. Sterker nog, ze misleiden doordat ze een onterecht gevoel van volledigheid van de definitie geven.

Wanneer een ontwerp wordt gemaakt dan blijkt dit meestal tamelijk omvangrijk. Beschrijvingen van tientallen tot honderden pagina’s zijn zeker geen uitzondering. Deze ontwerpen bevatten noodzakelijkerwijs fouten en inconsistenties.

Vage, complexe, foutgevoelige ontwerpen zijn nauwelijks geschikt om als uitgangspunt te dienen voor een programmeur. En hij wordt dikwijls nog met een ander obstakel opgescheept. In meer dan de helft van de gevallen is het zijn taak om een bestaand systeem uit te breiden of aan te passen. De documentatie daarover is vaak gigantisch, vrijwel altijd ondoorzichtig en meestal achterhaald. Dergelijke programmeurs zijn niet te benijden, en het is niet verbazingwekkend dat vele softwareprojecten niet slagen.

Een ander probleem waarom we software niet goed beheersen is dat de taken die de software zou moeten overnemen niet goed worden begrepen. Circa. twee jaar geleden sloeg hier in Eindhoven een bus op hol. Een niet onwaarschijnlijke reconstructie van de gang van zaken is de volgende. De bus was uitgevoerd met een veiligheidscircuit, dat er voor zorgde dat de bus vol gas gaf wanneer de hoofdcomputer was uitgevallen. De gedachte was dat een bus op een overweg met een uitgevallen hoofdcomputer weg zou moeten kunnen. Helaas viel de hoofdcomputer uit op het meestal drukke busstation in Eindhoven, waarschijnlijk door een elektromagnetische puls. De veiligheidsfunctionaliteit was terloops ingebouwd, en slechts bekend bij de constructeurs. De chauffeur was niet op de hoogte, en wist niet wat hem overkwam.

Een ander veel voorkomend probleem is de vergissing, of nog een slag erger, conceptueel onbegrip. Ook al worden de doelen die de software moet realiseren goed begrepen, dan nog kan het vergeten van één symbool in de programmatekst voldoende zijn om de computer volledig van slag te brengen. Het beroemde voorbeeld is de Mariner 1 raket uit 1962, waar per ongeluk een minteken in het programma was vergeten. Dit was niet ontdekt bij zorgvuldige inspectie, en de raket is uit de koers geraakt en tot ontploffing gebracht. Dit voorbeeld lijkt erg op de eerste Ariane 5 raket die in 1996 vanwege een softwareprobleem uit de koers raakte en ook is opgeblazen.

Een voorbeeld waarbij er conceptuele fouten gemaakt werden betrof de fout in het vermenigvuldigingscircuit van Intel’s Pentium processor. Voor de vermenigvuldiging werd gebruik gemaakt van een tabel. De ingenieurs meenden dat in dit geval een paar posities in de tabel niet hoefden te worden ingevuld, en zetten op die plaatsen de waarde 0. Dat leidde tot fouten in sommige vermenigvuldigingen. Kleine fouten weliswaar, maar wel fouten waarmee de processor onbruikbaar werd voor rekenintensieve taken. De vervanging van foute Pentiums door correcte heeft Intel ca. 1 miljard gulden gekost. En ze waren gewaarschuwd. Ook in de Intel 80486 processor hadden zich soortgelijke problemen voorgedaan. Als reactie heeft Intel in de Verenigde Staten en in Israël een drietal onderzoekslaboratoria opgezet om methoden te ontwikkelen die dit type fouten moeten gaan voorkomen.

Hoe ingewikkeld is software? Dat is een moeilijke vraag waarop geen afdoende antwoord bestaat. Maar beschouw eens de eenvoudige taak om 10 getallen, ieder groter gelijk 0 en kleiner dan 100 te sorteren. Zelfs een mens kan dit in betrekkelijk korte tijd goed uitvoeren. Als we van alle mogelijke rijtjes van lengte 10 apart willen nagaan of ze goed worden gesorteerd, moeten zelfs de snelste computers op aarde nog vele eeuwen rekenen. In het algemeen zijn de taken die door computers worden uitgevoerd gigantisch veel ingewikkelder. Computers sorteren routinematig telefoonboeken, en ook dit wordt beschouwd als een eenvoudige taak. Het voorbeeld om getallen te sorteren laat zien waarom de complexiteit van software zo wordt onderschat. Men denkt dikwijls in termen van één of enkele voorbeelden over wat software zou moeten doen, in plaats van te denken over ieder mogelijk gedrag onder alle denkbare omstandigheden.

Overigens zijn er ongetwijfeld vakgenoten die zullen beweren dat we al sinds jaar en dag weten hoe de correctheid van een sorteeralgoritme bewezen kan worden, en dat daarom sorteren niet kan dienen om de complexiteit van software te illustreren. Deze zienswijze gaat echter voorbij aan mogelijke vergissingen in de programmatekst, fouten in het bewijs van een concrete formulering van een sorteeralgoritme, fouten in de compiler en in de processor waarop het programma wordt uitgevoerd.

Een andere tegenwerping is dat we wel weten of een sorteeralgoritme correct is wanneer we het enkele keren hebben getest. Als ervaringsfeit lijkt dit in het algemeen wel juist voor sequentiële programma’s. Maar we begrijpen dit fenomeen niet echt. Bij mijn weten bestaat er echter geen enkel praktisch bruikbaar inzicht hoe vaak en op welke wijze een programmatekst moet worden getest om te mogen concluderen dat ook voor alle niet geteste gevallen het programma goed werkt. Ik heb in deze mijn hoop gevestigd op de Kolmogorov complexiteit, die iets zegt over de inherente complexiteit van strings, omdat ik geen andere manier zie het probleem aan te pakken.

Voor parallelle systemen lijkt het niet waar dat testen afdoende alle fouten aan het licht brengt. Een voor mij tamelijk schokkend voorbeeld kwam ik tegen toen ik met Wim Hesselink werkte aan een probleem waarvoor we een parallel, waitfree algoritme zochten. Wim en ik formuleerden beiden een oplossing, waarbij mijn oplossing duidelijk efficiënter was. Nog voor ik de correctheid van mijn algoritme had bewezen – maar in de overtuiging dat het correct was – had ik mijn oplossing geïmplementeerd. Een cruciale stap in het algoritme was het reserveren van een vrij stukje geheugen. Bij het testen van het programma bleek dit één op de 5 miljoen maal fout te gaan. Toen ik na enkele dagen begreep wat er fout was, begreep ik ook dat ik geluk had gehad. Met iets andere test parameters had het probleem zich niet gemanifesteerd. En als ik mijn algoritme had ingebed in een groter geheel, dan hadden we de fout tijdens testen waarschijnlijk ook niet ontdekt. Het zou zich bij gebruik weleens hebben voorgedaan, maar daar het probleem niet reproduceerbaar is, zou het waarschijnlijk niet meer kunnen worden achterhaald. Wim Hesselink had inmiddels zijn variant correct bewezen, en ter controle het bewijs laten checken door de Boyer-Moore theorem checker. Daarin kwam na implementatie geen enkel probleem aan het licht.

Ik hoop dat ik duidelijk heb gemaakt dat de behoefte om systemen beter te beheersen zal toenemen. Verder heb ik betoogd dat de huidige manier van ontwikkelen en testen waarschijnlijk niet in deze behoefte kan voorzien. Aan ons is de taak tijdig kennis en technologie gereed te maken opdat we kunnen uitleggen hoe softwaregestuurde systemen te bouwen die zich wel volledig voorspelbaar gedragen.

Doen we dit niet, dan vrees ik voor een technologische achterstand die aanzienlijke consequenties kan hebben. Welk bedrijf zou de besturing en de metrostellen voor de noord/zuid as van de metro in Amsterdam mogen leveren? Zouden bedrijven in Nederland op kunnen tegen een bedrijf als GEC Alsthom die bovengenoemde bestuurdersloze metrolijn in Parijs heeft aangelegd, en kan garanderen dat de besturing geen fouten bevat? De grote softwaredienstverleners in Nedrland zullen het ook wel moeilijk krijgen wanneer ze blijven weigeren echte verantwoordelijkheid voor hun producten en diensten te nemen. We zullen bovendien nog veel geld moeten investeren in nieuwe spoorbanen als we de treinbeveiliging niet zo durven aanpassen dat de capaciteit boven de 20 treinen per uur per baan opgevoerd kan worden.

Welnu, hoe moeten we beheerst software construeren? Ik denk zelf dat het maken van precieze en compacte specificaties van gewenst gedrag van systemen het belangrijkste ingrediënt tot verbetering is. Implementaties zullen op basis hiervan moeten worden gemaakt, zodanig dat de relatie met de specificatie mathematisch kan worden aangetoond. Als ondersteuning van het opstellen van de specificatie kunnen gewenste eigenschappen worden geformuleerd, waarvoor de modale logica zeer geschikt is.

Onder het externe gedrag van een systeem versta ik alle communicaties van dat systeem met de buitenwereld. De buitenwereld kan bestaan uit mensen die het te bouwen systeem wensen te gebruiken, of andere systemen, die met het te bouwen systeem moeten samenwerken. De grondslag voor de in mijn ogen elegantste wijze van beschrijven is gelegd door Milner in 1973. Hij stelde dat de toen heersende visie over systemen, "je stopt er gegevens in, en na enige tijd komt er een antwoord uit en dan ben je klaar" in feite niet klopte met de realiteit. Ook in die tijd gedroegen computersystemen zich al als machines die continu met de buitenwereld communiceerden, via toetsenborden, verwisselbare schijven, en via de toen nog zeldzame computernetwerken. Hij stelde tevens vast dat parallellisme een overheersende rol speelt in computers, en dat computers zich nondeterministisch gedragen. Dit laatste stuit bij sommigen nog op weerstand en ongeloof. Een computer doet namelijk precies dat wat is voorgeschreven. Maar juist omdat er zoveel dingen tegelijkertijd gebeuren in een computer, en alles invloed op elkaar kan hebben, is het soms onvoorspelbaar wat een computersysteem feitelijk zal doen. Het is vergelijkbaar met het weer. De vleugelslag van een vogel kan uiteindelijk de doorslag geven voor een storm. Zo kan het exacte moment van een toetsaanslag, of zelfs de temperatuur in een computersysteem, bepalend zijn voor de keuzen die een computer zal maken bij de uitvoering van zijn programma.

Milner vatte zijn ideeën in 1980 samen in het boek Calculus of Communicating Systems, kortweg CCS. Een belangrijk idee van CCS is dat communicatie synchroon gebeurt, d.w.z. als twee partijen willen communiceren, dan gebeurt dat onmiddelijk op een of andere magische wijze. Hiermee abstraheert hij van de soms subtiele wijze waarop systemen met de buitenwereld communiceren, en daarmee wordt het des te geschikter als abstract beschrijvingsmiddel voor systemen. Een ander belangrijk idee van Milner is dat van een interne actie. Dit is een actie die weliswaar in een machine plaats vindt, maar die we niet kunnen of willen observeren. Hiermee kunnen we het voor ons niet relevante gedrag van een systeem als intern beschouwen, en ons alleen richten op de externe acties van een systeem.

Een aanzienlijk aantal onderzoeksgroepen heeft de ideeën van Milner opgepakt. Twee wil ik er noemen. De eerste is de groep die de taal LOTOS heeft gedefinieerd, rond Chris Vissers en Ed Brinksma. Zij zagen de potentie van CCS om als abstract specificatieformalisme te dienen voor complexe systemen, en hebben met aanzienlijke krachtsinspanning de taal LOTOS voorzien van een goede taaldefinitie en krachtige computerhulpmiddelen. Natuurlijk heeft de taal LOTOS zijn tekortkomingen. Deze zouden moeten worden weggewerkt, door gebruik te maken van de ervaring die is opgedaan met de taal. De verdere ontwikkeling van LOTOS heeft in Nederland echter niet zo’n hoge prioriteit, en is overgenomen door enkele groepen verspreid over Europa.

Een andere groep die werkte in de lijn van Milner concentreerde zich rond Jan Bergstra en Jan Willem Klop in Amsterdam. Hier werd de Algebra van Communicerende Processen (ACP) onderzocht, voornamelijk als mathematisch fenomeen. Net als Milner richtte men zich alleen op de kern, waarbij zoiets essentieels als data werd weggelaten. Men werkte hard om een wiskundig zo elegant mogelijke algebra in elkaar te zetten waarover zoveel mogelijk mathematisch inzicht moest worden verkregen. Indrukwekkende resultaten zijn de tralie van procesequivalenties ontwikkeld door Rob van Glabbeek, en het aanzetten van een lange reeks van publicaties over de beslisbaarheid van procesalgebra’s door Jan Willem Klop, c.s.

In 1990 hebben Alban Ponse en ik de taal µCRL gedefinieerd, die het midden houdt tussen LOTOS en ACP, en in veel aspecten lijkt op de door Sjouke Mauw en Gert Veltink ontwikkelde taal PSF, al is µCRL bewust veel eenvoudiger gehouden.

Zowel met behulp van LOTOS, µCRL als met PSF is aangetoond dat van grote systemen het externe gedrag uitstekend is te specificeren. Mijn favoriete voorbeeld is nog altijd de Kidcom, een door Philips ontwikkeld elektronisch speelgoed bedoeld voor meisjes. De specificatie van het externe gedrag van de Kidcom, door Jan Springintveld, Jaco van de Pol en mij, heeft voor mij onomstotelijk aangetoond dat specificaties in een van de bovengenoemde talen een grote bijdrage kunnen leveren. Om de specificaties goed op te schrijven, moesten we vragen stellen. De consternatie die daaruit ontstond maakte duidelijk dat de ontwerpers van de Kidcom, die overigens absoluut capabel waren, een ontwerp-probleem hadden. Ze onderschatten de complexiteit van hun ideale speelgoed volkomen, en bleken geen methodes te hebben om voortgang in het ontwerp goed vast te leggen. Daardoor ontstond een cultuur waarin het mogelijk was ieder besluit over de beoogde werking van het apparaat op ieder moment te herroepen. Alle activiteit heeft geleid tot een grappig product, dat overigens slechts een klein deel van de door ons gespecificeerde functionaliteit bevat. En dat terwijl wij ooit geweigerd hadden alle door de ontwerpers beoogde functionaliteit te specificeren, omdat we het allemaal veel te groot en ongestructureerd vonden.

Gedragsspecificaties blijken nogal snel erg groot te worden, waarbij overzicht verloren gaat en fouten ontstaan.

Specificaties worden lang omdat computergestuurde systemen meestal niet netjes ontworpen worden, maar organisch groeien. Wanneer uiteindelijk alsnog geprobeerd wordt een specificatie te maken, wordt deze lang en complex. Een ander probleem is dat sommige systemen zoveel uiteenlopende functionaliteit krijgen toegedacht, dat het noodzakelijkerwijs lang duurt alles goed gespecificeerd te krijgen. Deze rede is gemaakt met Microsoft Word. Alhoewel ik deze tekstverwerker in verschillende versies al ruim tien jaar gebruik, kan ik er niet goed mee omgaan. De functionaliteit is te ingewikkeld, en vele mogelijkheden ongestructureerd.

Wanneer een systeem zo ingewikkeld is geworden dat het niet meer kan worden beschreven, dan duidt dit op een probleem met het systeem. Herontwerp is een van de beste opties, en meestal leidt dit tot een zeer drastische inkrimping van de gedragsbeschrijving, zonder dat er aan functionaliteit hoeft te worden ingeboet.

Een andere reden waarom gedragsspecificaties omvangrijk zijn is dat ze in aanzienlijke mate gedetailleerd zijn, want ieder aspect van het gewenste gedrag moet worden vastgelegd. Grote specificaties bevatten ook een groot aantal fouten. En specificaties waarvan men min of meer aanneemt dat er fouten in zitten kunnen niet goed dienen als ontwerp-voorschrift. Er moeten hulpmiddelen beschikbaar komen om fouten te vermijden of te verwijderen, en de huidige hulpmiddelen schieten tekort.

Bovendien hebben de huidige specificatietalen nog niet hun optimum bereikt. Talen als LOTOS en PSF hebben een lage informatiedichtheid per regel, waardoor zelfs betrekkelijk eenvoudige specificaties groot ogen. Alle bovengenoemde talen hebben als nadeel dat ze op een tamelijk onhandige manier met data omgaan. Ook voor alle andere specificatietalen kunnen reeksen van bezwaren worden aangevoerd, en er kan op dit gebied nog een hele evolutie worden verwacht.

Een bezwaar dat soms wordt aangevoerd tegen het gebruik van gedragsspecificaties is dat ze veel te determinerend zijn, en dat het niet mogelijk is implementatievrijheden aan te geven. Dit bestrijd ik. Samen met Dennis Dams hebben we een specificatie gemaakt van een toolset voor µCRL, waarin we door handig gebruik te maken van ongespecificeerde data parameters de door ons gewenste vrijheidsgraden van implementaties precies konden aangeven. Overigens bestaat er ook een aanpak voor dit probleem waarbij gebruik gemaakt wordt van implementatierelaties, en niet deterministische interne acties. Hiervan denk ik dat er inderdaad geen oplossing wordt geboden. Overigens heeft de exercitie samen met Dennis Dams wel duidelijk gemaakt dat het mogelijk is op zeer compacte wijze het gedrag van systemen te beschrijven, mits er een compact ontwerp aan ten grondslag ligt.

Een andere manier van specificeren komt voort uit de modale of temporele logica. Hierbij worden slechts aspecten van het systeemgedrag weergegeven. Een typisch voorbeeld zien we bij de treindienstregeling: als een sein op rood wordt gezet, moet het na enige tijd ook rood worden. Vooral in die gevallen waarin de functionaliteit van een systeem ons te machtig is, bieden dergelijke formules houvast. Ik meen echter dat de rol van dergelijke formules altijd een marginale zal blijven. Het is te moeilijk een volledig systeem te karakteriseren met deze formules, en daarmee zijn ze ongeschikt als primair ontwerp-hulpmiddel. Bovendien zijn ze problematisch vanuit het standpunt van de zogenoemde compositionele bewijsmethode. Deze methode zegt dat je eerst van de onderdelen van een systeem de correctheid bewijst, en op basis daarvan van steeds grotere samenstellingen.

Modale formules zijn wel zeer geschikt om aan het begin van een project systeemeisen te formuleren. Na het ontwerp van het systeem kunnen deze formules als nuttige extra controles worden gebruikt.

Laten we aannemen dat we er in zijn geslaagd de specificatie van een systeem goed onder woorden te brengen. Het is daarmee helemaal nog niet gezegd dat een goed werkend systeem zal worden gerealiseerd. Het is nu zaak de juiste algoritmes, protocollen en fout-afhandelingsmechanismen op te stellen. Een conceptuele fout is in deze eenvoudig gemaakt. Een voorbeeld hiervan ontdekten we toen we de nieuwe Philips Remote Control standaard doorrekenden. Een bepaald bit werd soms gebruikt als bevestiging van juiste ontvangst, en soms gebruikt als verzoek om de transmissie van gegevens te beëindigen. Men had het systeem niet voldoende begrepen om in te zien dat het mogelijk was dat één partij de transmissie kon wensen te beëindigen, terwijl de andere partij dit kon opvatten als de bevestiging van de aankomst van een verloren gegaan bericht.

De standaardmethode om foute implementaties te vermijden bestaat uit het geven van een bewijs dat een voorgesteld algoritme of protocol correct werkt. De klassieke theorie hiervoor bestaat uit de Floyd/Hoare logica’s, uitgebreid voor parallelle systemen met Gries-Owicki achtige technieken.

De Floyd/Hoare achtige methodes richten zich voornamelijk op de pre-Milneriaanse visie van systemen. Wanneer systemen beschouwd worden in Milner’s stijl, dan blijken de primaire procescalculi niet afdoende te zijn om in acceptabele tijd correctheid van zelfs de meest primaire algoritmes te bewijzen. De groep rond Nancy Lynch op het MIT zag dit als een van de eersten, en ontwikkelde de notie van een I/O automaat, met bijbehorende bewijsmethoden rond de notie van trace equivalentie tussen processen. Uitgaande van de primaire procescalculi hebben wij gelijksoortige methoden ontwikkeld waarmee gedistribueerde algoritmes te bewijzen zijn in branching of zwakke bisimulatie semantiek. Inmiddels kunnen op tamelijk systematische wijze allerlei gedistribueerde parallelle algoritmes correct worden bewezen. Wat ontbreekt is een classificatietheorie met betrekking tot algoritmes. Hiermee kunnen we leren de essentiële structuur van deze algoritmes te begrijpen.

Bovendien zijn er verder allerlei algoritmes waarvan het nog steeds een open probleem is er een mooi en inzichtelijk bewijs van te geven. Als typisch voorbeeld wil ik Bloom’s register noemen. Bloom beschrijft een simpele, en tevens effectieve manier om van twee single-writer, multi-reader registers, één two-writer, multi-reader register te maken. Ik ken geen elegante methode om van dit algoritme de correctheid te bewijzen, maar meen dat prophecy variabelen hier een uitstekende leidraad vormen. Prophecy variabelen nemen in de loop van een proces alvast een waarde aan die aangeeft wat er later zal gaan gebeuren. Binnen de I/O-automatentheorie blijken deze een essentieel onderdeel van de methodologie, al worden ze in voorbeelden vrijwel niet gebruikt. In de procesalgebra worden ze tot nu toe volledig genegeerd.

Bewijsmethoden worden vrijwel niet in de alledaagse programmeerpraktijk gebruikt. In mijn ogen is dit voornamelijk de schuld van de opleidingen informatica. Redeneren over programma’s vereist een gedegen training en ervaring, zoals we ook jarenlang onze scholieren erin trainen om te gaan met polynomen, differentiaalvergelijkingen en matrices. Met uitzondering van de door Dijkstra geïnspireerde opleidingen, zoals hier aan de TUE, komt redeneren over programma’s nauwelijks aan de orde, maar gaat de meeste aandacht uit naar het snel construeren van een programma. Inzet van bewijstechnieken zou buitengewoon veel tijd van programmeurs vergen, voldoende om de methode als onpraktisch en veel te duur te kenschetsen.

Programma’s zijn ook vaak te groot of te onhanteerbaar om met de beschikbare technologie correct bewezen te worden. In zo’n geval kan het maken van een model van de software uitkomst bieden. Bij algoritmes is dit al algemeen gebruik want een algoritme is immers slechts een abstracte beschrijving van de ervan af te leiden concrete programma’s. Ook protocollen worden op een abstract niveau beschreven, op basis waarvan de concrete protocollen te bouwen zijn. Veel vaker zouden we ook van concrete software een model moeten maken, waarmee we kunnen aantonen dat de software geen conceptuele fouten vertoont. Voor een modulair autoliftsysteem hebben we op deze wijze zonder noemenswaardig veel inspanning een probleem boven water gehaald dat de constructeurs veel last had bezorgd.

Ook modellen zijn vaak te omvangrijk voor handmatige analyse. Het gebruik van geautomatiseerde hulpmiddelen of tools is daarom noodzakelijk. Ondanks het feit dat de duizelingwekkende voortschrijding van de capaciteiten van computers een sterke rugwind veroorzaakt, moet hier worden vastgesteld dat dit vakgebied in de kinderschoenen staat, alhoewel er inmiddels enkele successen zijn geboekt.

Laat ik beginnen te zeggen dat ik, wanneer ik over analysetools spreek, niet verwijs naar checkers van statische eigenschappen, zoals syntax checkers of typeringscheckers. Deze hulpmiddelen werken in het algemeen uitstekend, maar zijn niet bedoeld om dynamische eigenschappen te onderzoeken.

De meest gebruikte analysetools zijn gebaseerd op de exploratie van een toestandsruimte. Het idee is dat een systeem telkens bij iedere activiteit in een volgende toestand overgaat, waarin andere activiteiten mogelijk zijn. Het tellen tot 10 kan gezien worden als een toestandsruimte met 10 toestanden. In de eerste toestand kan 1 worden geteld, en gaan we naar toestand 2. In toestand 2 tellen we 2 en gaan naar toestand 3, enzovoort.

Als een systeem minder dan ca. 10 miljoen toestanden heeft, dan kan de totale toestandsruimte worden berekend, en kan vrijwel ieder aspect van het gedrag van het systeem diepgaand worden geanalyseerd. Binnen enkele jaren zal dit zijn opgelopen naar 100 miljoen, of zelfs 1 miljard toestanden. Helaas voor deze aanpak, heeft vrijwel ieder denkbaar systeem veel meer toestanden. Laat 20 mensen tegelijkertijd tot 10 tellen en de toestandsruimte past niet in het gezamenlijke werkgeheugen van alle computers nu op aarde.

Dit is ook een belangrijke reden om modellen te gebruiken. Met enige handigheid kan een model zo worden opgesteld dat de bijbehorende toestandsruimte relatief klein blijft, onder behoud van de te onderzoeken eigenschappen van een systeem. Wanneer ook dit niet werkt, kunnen we slechts een deel van het systeem beschouwen. De achterliggende gedachte is dat als er in het hele systeem problemen zijn, ze ook in een gereduceerde versie aanwezig zijn. We zouden in plaats van 20 tellende mensen er 3 kunnen bestuderen. Het er bij behorende toestandsysteem heeft 1000 toestanden, en dat heet tegenwoordig klein.

Om de analyse op grotere toestandsruimtes te plegen moeten we gebruik maken van de structuur van systemen. Er bestaan op dit gebied twee hoofdstromen. De eerste gebruikt een codering in propositielogica voor de toestandsruimte. Door middel van deze techniek zijn toestandsystemen tot 10¹³⁰⁰ toestanden geanalyseerd. Zelf hebben we met dergelijke technieken ooit het veiligheidssysteem van de stations Hoorn-Kersenboogerd en Heerhugowaard doorgerekend. Van deze laatste schatten we de toestandsruimte op 10¹⁰⁰⁰ toestanden. Helaas is het succes van het gebruik van deze methode niet voorspelbaar. Soms blijkt codering door middel van propositielogica niet eens krachtig genoeg om systemen met enige honderden toestanden door te rekenen. Het boeken van voortgang op dit gebied gaat moeizaam. Er bestaat behoefte aan veel krachtiger algoritmes om proposities te bewijzen. Fundamenteel begrip op dit gebied blijkt echter nauwelijks te bestaan. In mijn ogen is er een lacune in de vakgebieden logica en automatisch redeneren: ze geven geen uitsluitsel hoe men het best naar een bewijs kan zoeken voor een gegeven logische formule. Praktische voortgang wordt hier ernstig gehinderd door gebrek aan adequate theorie. Een teken aan de wand vind ik nog altijd dat pas in 1991 werd gepubliceerd dat waarheidstafels veel efficiënter kunnen zijn dan tableaus, een feit dat in mijn ogen al 50 jaar algemeen bekend had mogen zijn.

De andere hoofdstroom probeert het maken van de toestandruimte zo lang mogelijk uit te stellen door zoveel mogelijk te analyseren aan het gegeven systeem zelf. Soms is dit zelfs noodzakelijk, omdat een systeem parameters bevat die open zijn gelaten. Gedistribueerde systemen moeten vaak werken voor ieder mogelijke netwerkconfiguratie en ieder mogelijk aantal deelnemende processen. Een bezwaar van deze methode is dat de beschrijving van een systeem niet erg homogeen is, wat het moeilijker maakt om de analysetechnieken te formuleren. Dit is de reden dat ik er nu de voorkeur aan geef een systeem eerst naar een lineaire proces operator (LPO) te vertalen omdat die een simpele structuur heeft en grote systemen goed kan representeren.

Om analyses op systeembeschrijvingen of lineaire proces operatoren automatisch uit te voeren moet gebruik gemaakt worden van technieken zoals herschrijven, unificatie en het automatiseren van inductiebewijzen. Het effectief hanteren van deze technieken valt echter niet mee. Bij onze eigen experimenten hebben we tot nu toe slechts automatisch de confluentie van twee parallelle queues aangetoond en hebben we het wel erg eenvoudige SLIP protocol correct bewezen. Internationaal gezien lijkt met name het STEP systeem uit Stanford zich georiënteerd te hebben op deze aanpak. Hier wordt enig succes geclaimd inzake de automatische generatie van invarianten.

Tot nu toe heb ik mij voornamelijk gericht op de vraag hoe conceptuele fouten aangepakt moeten worden. Vergissingen of slordigheden komen minstens zo vaak voor in een programma. Geen van de algemeen gebruikte methoden is afdoende geschikt om alle vergissingen uit een programmatekst te halen. Het enige geschikte middel dat ik ken zijn automatische bewijscheckers, zoals Isabelle, PVS en Coq, die mede zijn geïnspireerd door het werk van De Bruijn aan Automath. Voor het gebruik van deze checkers is het nodig dat de correctheid van een programma is geformuleerd en bewezen. Deze checkers controleren daarna of iedere bewijsstap volgens strikt logische regels is gezet. Bij een handmatig bewijs kan een verschrijving nog eenvoudig over het hoofd worden gezien. Maar de checker zal een probleem genadeloos aan het licht brengen.

Een checker als Coq biedt nog een additioneel voordeel. Wanneer een bewijs van correctheid is gecheckt, kan het bij het programma worden gevoegd. De afnemer kan onafhankelijk nagaan met een redelijk eenvoudig programma of het bewijs inderdaad een correct bewijs is. Dit zou bijvoorbeeld het dilemma op kunnen lossen dat bestaat bij projecten zoals de beweegbare afsluitdeuren in de Nieuwe Waterweg. Rijkswaterstaat is ongetwijfeld bereid te betalen voor de software samen met een controleerbaar bewijs van correctheid. Maar omdat niemand dit kan leveren, is Rijkswaterstaat gedwongen de software zonder garantie van correctheid te laten maken. Volgens de standaard aanbestedingsprocedure gebeurt dat door de goedkoopste leverancier.

Helaas is het zo dat er slechts op zeer kleine schaal wordt geëxperimenteerd met volledig correct bewezen programma’s, en voor zover ik weet bestaat er in Nederland niemand met de ambitie om aan de technologie te werken bewijscheckers op omvangrijke programma’s toe te passen.

Welnu, wat ga ik zelf doen? Het doel van deze rede is immers om mijn eigen ambities, doelstellingen en met name concrete activiteiten aan U voor te leggen. Ik denk dat ik mijn lange termijn doelstelling meer dan duidelijk heb gemaakt. Ik wil onderzoek doen opdat het mogelijk wordt betrouwbaardere programma’s en computergestuurde systemen te maken.

Voor de korte termijn kan ik aanzienlijk concreter zijn. Mijn huidige doel is om aan te tonen dat door gebruik van symbolische methoden in de breedste zin van het woord beduidend grotere systemen dan nu automatisch kunnen worden geanalyseerd. Hierbij moet de effectiviteit uiteindelijk zo groot zijn, dat gebruik bij feitelijke softwareontwikkeling als vanzelfsprekend zal worden ervaren.

Het is voor mij onmogelijk iedereen te danken die dat toekomt. Toch wil ik de Jenaplanschool in Berlikum (Frl.) bedanken, waar ik meen te hebben geleerd zelf mijn doelen te kiezen en vooral zelfstandig, zonder externe druk, aan het bereiken ervan te werken. Het Stedelijk Gymnasium in Leeuwarden heeft mij geleerd wat werken is. Het heeft ook de kiem van mijn enthousiasme voor de informatica gelegd. De wiskundeleraren Hoepman en Scholl hadden voor geïnteresseerde leerlingen een cursus programmeren in de Nederlandstalige programmeertaal Ecol georganiseerd.

Daarom besloot ik informatica aan de Universiteit Twente te studeren. Ik heb er veel geleerd, maar ik meen de Universiteit Twente toch vooral te moeten bedanken voor de diepe frustratie die ik er heb opgelopen. Bij mijn afstuderen voelde ik mij wat men noemt een hacker, best in staat indrukwekkende programma’s te schrijven, maar niet in staat een professioneel en betrouwbaar product te leveren. Om ooit een echte software ingenieur te worden, moest ik mij verder scholen.

Nu had ik terloops gehoord van het Centrum voor Wiskunde en Informatica (CWI), een onderzoeksinstituut in Amsterdam. Informatica had mijn interesse en wiskunde leek mij zeer noodzakelijk voor mijn verdere ontwikkeling. Ik heb er gesolliciteerd, en werd zonder veel omhaal door prof.dr. J.A. (Jan) Bergstra aangenomen om te werken in zijn onderzoeksgroep. In deze groep werkten twee promovendi, Rob van Glabbeek (nu onderzoeker in Stanford) en Frits Vaandrager (nu hoogleraar in Nijmegen). Er heerste een ongekende onderzoekssfeer, en het is vooral Frits geweest, en hiervoor zal ik hem altijd dankbaar blijven, die mij heeft geleerd wat het betekent onderzoek te doen, en hoe je daarover artikelen moet schrijven. Van Jan Bergstra heb ik vooral geleerd over onderzoek en onderzoekers te denken. Mijn dank gaat ook uit naar prof.dr. J.W. (Jaco) de Bakker, die op het CWI de context schiep en schept waarbij maximale aandacht voor het onderzoek mogelijk is, zelfs gedurende de steeds weerkerende reorganisaties.

Ik zou hier prof.dr. J.C.M. (Jos) Baeten niet mogen vergeten. Niet alleen was hij mijn co-promotor, maar vooral dank ik aan hem zijn initiatief om het CWI en mij te vragen om mij één dag per week ter beschikking te stellen om aan deze universiteit te werken.

Dank gaat ook uit naar mijn collega’s niet alleen binnen het thema SEN2 op het CWI en in de formele methoden groep hier in Eindhoven, maar ook alle daarbuiten. Er is nog zoveel te doen, dat we elkaar, elkaars ideeën en elkaars motivatie hard nodig zullen hebben.

Natuurlijk gaat ook mijn dank uit naar mijn vrouw Paula, onze kinderen, Gijs en Anna, mijn ouders, Stoffer en Wytske Groote, alsmede de rest van mijn familie, vrienden en kennissenkring.

Gelukkig is op deze universiteit het ‘hora est’ weer ingevoerd. Het lijkt me daarom aardig deze rede in het Latijn te beëindigen.

Gratias omnibus debeo qui me hominum qui sum fecerunt. Me spero fore auctorem dignum investigationis mihi iussae et attribuire omnes facultates meas quibus omne genus humanum uti potest. Omnia instrumenta mihi parata quam optimae possum adhibebo.

Dixi.