De stormvloedkering in de Nieuwe Waterweg is het sluitstuk van de Deltawerken. De kolossale, 1,3 miljard gulden kostende constructie moet de regio Rotterdam (ruim 1 miljoen mensen, industrieën, havens) vanaf 1997 bij storm en extreem hoogwater tegen de zee gaan beschermen. Indertijd is voor een stormvloedkering gekozen om te voorkomen dat er in de bebouwde kom van de Rijnmond dijken op Delta-hoogte zouden moeten worden aangelegd.
De kering bestaat uit twee enorme stalen deuren (210 meter lang, 22 meter hoog, 15 meter breed) die aan 237 meter lange beweegbare stalen armen zijn bevestigd. De armen draaien met behulp van een 'schoudergewricht': een tien meter groot gietijzeren bolscharnier in dito achterstoel, tot op de millimeter gepolijst en voorzien van een speciale op molybdeen gebaseerde glijlaag die de twee gewrichtsdelen soepel over elkaar laat bewegen. Het geheel is gevat in een zware betonnen fundering die de kering tegen een waterdruk van tienduizenden tonnen moet kunnen beschermen.
De 15 duizend ton wegende deuren zitten in ruststand opgeborgen in speciale droogdokken. Bij hoogwater worden de dokken onder water gezet, waardoor de holle deuren gaan drijven. Via door motoren aangedreven locomobielen worden de deuren dan de rivier in gedraaid. Als ze elkaar midstrooms naderen, worden ze met water gevuld waardoor ze afzinken op een betonnen drempel. Om de kering weer te openen worden de deuren leeggepompt en ingedraaid.
Het ontwerp komt voort uit hoge, deels tegenstrijdige eisen. De kering moet zowel de 360 meter brede Nieuwe Waterweg kunnen afsluiten, alsook de scheepvaart op de drukke rivier zo min mogelijk hinderen (door bijvoorbeeld betonnen pijlers in de rivier, zoals bij de stormvloedkering in de Theems). De 'sluitfrequentie' is bepaald op 0,1 keer per jaar. Hij zal dus naar verwachting eens per tien jaar worden gesloten; over vijftig jaar eens per vijf jaar, als de stijging van de zeewaterspiegel tenminste doorzet.
Centraal in de ontwerpfilosofie van de stormvloedkering staan faalkansen. Van elk element van de constructie, inclusief de factor van het menselijk tekortschieten, is uitgerekend hoe vaak het mis mag gaan. De constructie zelf mag eens in de een miljoen jaar bezwijken. Het sluiten van de kering mag eens per duizend keer mislukken. Het openen van de deuren maar eens per tienduizend keer: 'klemmende deuren' kosten de haven miljoenen per dag, daarnaast zouden stormvloedkering en dijken het kunnen begeven wanneer de zeewaartse waterdruk achter de kering te hoog zou oplopen.
De introductie van faalkansen hield een nieuwe manier van ontwerpen in. Vroeger werkten de ingenieurs met tamelijk willekeurige veilige marges, wat leidde tot overdimensionering: constructies werden hoger, dikker en sterker dan strikt genomen nodig was. Die aanpak is natuurlijk duur. Op basis van faalkansen worden de componenten nu meer in optimale samenhang ontworpen, waarbij goedkope onderdelen sterker en moeilijke of dure onderdelen wat zwakker kunnen worden uitgevoerd zonder dat het totale ontwerp uit evenwicht raakt. Zo is de betrouwbaarheid van het ontwerp beter te bepalen, al wordt die betrouwbaarheid er niet extra door vergroot.
Om menselijke fouten uit te sluiten is vanuit de faalkans-benadering ook besloten de bediening van de kering volledig te automatiseren. Een beslis- en besturingssysteem bepaalt zelf of de deuren gesloten moeten worden, en stuurt vervolgens de motoren en de pompen van de deuren aan. Ook bewaakthet systeem de correcte procedures, het waarschuwt bijvoorbeeld tijdig de diverse autoriteiten. Het systeem maakt bij dat alles onder meer gebruik van de waterstanden uit de regio Zuid-Holland en Zeeland, KNMI-weersvoorspellingen, maanstanden en gegevens over de directe omgeving van de kering. Omdat het systeem menselijk ingrijpen uitsluit (afgezien van een noodstop), moet de betrouwbaarheid van de software optimaal zijn.
Om die betrouwbaarheid zo groot mogelijk te maken schakelde softwarehuis CMG, dat het systeem gaat ontwikkelen, een team UT-informatici in. Dat gebeurde met name vanwege de Twentse know-how op het gebied van formele methoden: wiskundige technieken/modellen en ondersteunende software die het ontwerpproces van software van een wetenschappelijk fundament voorzien, en derhalve de betrouwbaarheid van het ontwerp kunnen maximaliseren.
Vanuit CMG werken zeven software-engineers aan de klus. Vanuit INF wordt binnenkort drs. Pim Kars (Tele-Informatica en Open Systemen) full-time bij CMG gedetacheerd. Daarnaast zijn ir. Wil Janssen (Software Engineering en Theoretische Informatica), voor de startfase, en dr. Job Zwiers (SETI) en prof.dr. Ed Brinksma (TIOS) als adviseurs bij het project betrokken. 'Als derde-geldstroomproject is dit voor ons een nogal uitzonderlijk geval: het is geen pure research, maar een concreet project dat over twee jaar af moet zijn', vertelt Brinksma. De stormvloedkering, waarvan de bouw in 1991 is begonnen, moet namelijk medio 1997 worden opgeleverd.
Brinksma gelooft dat de UT een zinvolle bijdrage kan leveren: 'Wij beschikken over geavanceerde middelen om software te ontwerpen en te analyseren, en die expertise brengen we in om de kwaliteit van het produkt te verbeteren.' Het ontwerp wordt geanalyseerd om te zien of de eigenschappen corresponderen met de gestelde taken, en gestructureerd door de inzet van wiskundig precieze methoden. Met speciale software zal de gestelde specificatie gecontroleerd worden op consistentie en volledigheid.
Janssen vult aan: 'Door het met formele methoden analyseren en structureren van het systeemontwerp met formele methoden is software-ontwikkeling niet langer een proces van trial and error.' En dat is een pre, want met standaard-software valt de vereiste betrouwbaarheid niet te halen. Overigens is de precieze faalkans van software moeilijk in te schatten. 'Het gaat bij software om systematische fouten en die zijn erg moeilijk te analyseren', aldus Janssen. En Brinksma: 'Bij de gegeven faalkansen betekent dat in de praktijk dat je het systeem zo betrouwbaar mogelijk moet maken.'
De UT-ers programmeren niet zelf, ze begeleiden de software-engineers van CMG bij het systeemontwerp. Er ligt nu een 700 pagina's dikke functionele specificatie (in natuurlijke taal en in de vorm van data-flow-diagrammen). 'Zulke specificaties zijn echter over het algemeen onvolledig, onvoldoende nauwkeurig en inconsistent', zegt Zwiers. Het UT-team zal het boekwerk helpen omzetten in een formele specificatie die controleerbaar is op consistentie en volledigheid. Dat is tevens de hoofdmoot van het werk. 'Het eigenlijke schrijven en implementeren van het programma zijn in feite maar een klein onderdeel van het ontwerpproces', aldus Zwiers.
Brinksma: 'Zo'n formele specificatie is eigenlijk een precieze definitie van het probleem dat je wilt gaan oplossen. De gestructureerde definiëring van een probleem is feitelijk al een deel van de oplossing, doordat je de zaak helder maakt. Het vergt wel een investering in het voortraject, die je weer terugververdient bij het schrijven en testen van het uiteindelijke programma. Het is reculer pour mieux sauter.' Vaak gooien bij de inzet van formele methodes de factoren tijd & geld echter roet in het eten.
De inzet van formele methoden bij software-ontwikkeling is in Nederland nog geen usance, zeggen de UT-ers. 'Nederland heeft eigenlijk geen echte software-industrie. Softwarehuizen doen vooral op nogal ambachtelijke manier aan administratieve automatisering, en daar hoef je niet alles voor uit de kast te halen. Ook bij complexe ontwerpen worden formele methoden niet vaak ingezet, en als dat wel gebeurt, is dat meestal wanneer het te laat is', zegt Brinksma. 'Daarom is dit project uniek.'
De INF-ers zijn dan ook zeer in hun nopjes. 'Het grote voordeel van ditproject is dat niet winstgevendheid maar betrouwbaarheid de doorslaggevende factor is. Betrouwbaarheidscriteria zijn belangrijker dan financiële aspecten. Dat niet op het scherp van de snede wordt gecalculeerd, biedt goede kansen voor inzet van formele methoden', zegt Brinksma. En hoewel het 'geen makkie' is, is het systeem ook niet zo complex dat je niet weet hoe je het aan moet pakken. 'We weten in principe hoe we het moeten doen.'
Een ander voordeel voor de UT is dat het een 'prettig concreet en aansprekend project' is. 'Ons werk is normaal gesproken tamelijk onzichtbaar. Van een geweldig complex software-systeem is voor de leek meestal niet meer te zien dan het computerschermpje dat die software verbergt. Als je hier mee scoort ben je ook meteen goed zichtbaar', zegt Janssen. 'We kunnen straks in ieder geval wijzen op die enorme technische constructie, al hebben we met de deuren en de bolscharnieren verder weinig te maken.'
De UT-ers zijn optimistisch over de samenwerking met de software-engineers van CMG. 'De mensen bij CMG hebben een positieve instelling tegenover de inzet van formele methoden bij het systeemontwerp. We ervaren een echte interactie. We zijn er niet alleen bijgehaald om de offerte aan Rijkswaterstaat op te krikken', beweren ze. 'En voor onszelf is het heel leerzaam om te ontdekken hoe we kunnen aansluiten bij ingenieurs op de werkvloer die niet getraind zijn in het toepassen van formele methoden.'
Een van de twee 'parkeerdokken' voor de beweegbare deuren van de stormvloedkering in aanbouw.
