Formele modelverificatie van stormvloedkering tot treinvolgsysteem

Gegarandeerd foutvrije software binnen tijd en budget, wie wil dat niet? Dat is de belofte die formele modelverificatie ons doet. Toch past de industrie deze tak van sport nog maar weinig toe, deels uit onbekendheid, deels uit angst voor de complexiteit van formele methodes. Aan de hand van drie praktijkvoorbeelden laat Franc Buve van Logica zien dat formele modelverificatie wel degelijk met succes in commerciële projecten toepasbaar is.

Modelverificatie is een onderdeel van modelgedreven ontwikkeling. Dit is een ruim begrip: de een vindt het maken van rudimentaire UML-diagrammen in een tekenpakket al modelgedreven ontwikkeling, een ander wenst daar pas van te spreken als uit de modellen automatisch grote delen programmacode zijn te genereren. Zelf beschouw ik als de essentie van modelgedreven ontwikkelen het gebruik van een specificatietaal of notatie om het systeem of delen daarvan te beschrijven op een manier die het mogelijk maakt het gedrag te voorspellen. Een dergelijk beschrijving noemen we een model en het controleren ervan op gewenst gedrag heet modelverificatie.

Afhankelijk van de gekozen notatie zijn er verschillende hulpmiddelen, of modelcheckers, waarmee we de verificatie geautomatiseerd kunnen uitvoeren. Dit varieert van eenvoudige consistentiecontroles, bijvoorbeeld of de uitstroom van de ene module wel klopt met de instroom van de andere, tot simulatie van modelgedrag, waarbij we kunnen zien of het ontwerp inderdaad doet wat we voor ogen hadden. Het summum van modelverificatie is een wiskundig bewijs van correctheid. Hiervoor zijn speciale specificatietalen nodig. Dit is het speelveld van de formele methodes.

Een consistentiecontrole vindt eigenlijk alleen de ’domme‘ fouten in een ontwerp, maar zegt niets over het gedrag. Een simulatie laat het gedrag van het systeem zien en legt daarmee ook functionele fouten bloot. De effectiviteit wordt echter beperkt door het aantal scenario‘s dat we simuleren. In de praktijk kunnen we slechts een fractie testen van de miljoenen of miljarden toestanden die een systeem kan hebben.

Alleen formele methodes geven volledige zekerheid dat het systeem zich gedraagt zoals gespecificeerd. Deze op wiskundige leest geschoeide technieken rekenen alle mogelijke toestanden van een systeem door. Hiervoor moeten we echter het model in een formele taal beschrijven, wat aanzienlijk meer inspanning vereist dan bijvoorbeeld modelleren in UML. Dit komt niet alleen doordat een formele taal moeilijk leesbaar is, maar vooral ook doordat een formele taal ondubbelzinnig is en het niet toestaat ook maar iets vaag of onduidelijk te laten.

Formele methodes hebben hun oorsprong in de academische wereld. De industrie heeft ze lang als onpraktisch beschouwd, omdat ze niet konden omgaan met de complexiteit van reële systemen. Dit beeld begint de laatste jaren echter te veranderen. Formele methodes worden nu ook met succes in de commerciële sector toegepast. De drempel om ze te gaan gebruiken, is echter nog hoog. Aan de hand van een drietal projecten uit mijn eigen praktijk wil ik illustreren hoe we formele methodes kunnen inzetten en waar we rekening mee moeten houden.

Desastreus

In 1995 zette Logica (toen CMG) zijn eerste stappen op het gebied van modelgedreven ontwikkeling bij het Beslis- en Ondersteunend Systeem (Bos) van de stormvloedkering in de Nieuwe Waterweg (de Maeslantkering). Daar moet de software uiteraard aan de hoogste betrouwbaarheidseisen voldoen. Om de gevraagde betrouwbaarheid van 99,999 procent (dat is een faalkans van 1 op 100 duizend, vergelijkbaar met eisen aan software voor een kerncentrale of spaceshuttle) aannemelijk te maken, besloten we om alle belangrijke onderdelen met formele methodes te modelleren. Hiervoor zijn we een samenwerking aangegaan met de Universiteit Twente. Zij hebben ons geadviseerd in de keuze van formele talen en geholpen met modelleren.

Voor het modelleren hebben we gekozen voor een combinatie van Promela en Z. Promela is een taal waarmee we gedrag in de vorm van toestandsovergangen goed kunnen modelleren. Z is juist geschikt om de bewerking van gegevens in modelvorm te gieten. Met deze combinatie hebben we vrijwel het gehele systeem, met uitzondering van de grafische userinterface, gemodelleerd. Promela hebben we toegepast om het dynamisch gedrag en de interface tussen processen te specificeren, Z om de functies te beschrijven.

Een van de eerste dingen waar we tegenaan zijn gelopen, is dat het ondoenlijk is om het volledige systeem in detail te modelleren. Niet alleen omdat dat zo veel werk is, maar vooral ook omdat het aantal toestanden van het volledige systeem zó groot is dat een modelchecker dat onmogelijk meer kan doorrekenen. De huidige generaties tools kunnen tot 1010 toestanden aan. Realistische systemen kunnen wel 101000 toestanden hebben. (Om een gevoel bij deze grootte te geven: het totaal aantal moleculen op aarde is in de ordegrootte van 1050.)

Deze toestandsexplosie is een bekende beperking van formele modelcheckers. Er zijn twee manieren om hiermee om te gaan. Ten eerste kunnen we door abstractie, het weglaten van details, het aantal toestanden drastisch verminderen. Bovendien maakt dit het model simpeler en beter te begrijpen. Ten tweede kunnen we een verdeel-en-heerstechniek toepassen. Hierbij modelleren en verifiëren we systeemcomponenten afzonderlijk; kleinere componenten hebben uiteraard minder toestanden. Voor het verifiëren van het totale systeem in samenhang zien we deze componenten vervolgens als black boxes waarbij alleen hun interface van belang is. De interne toestanden van die componenten tellen dan niet meer mee. Daarmee voorkomen we een toestandsexplosie.

Voor het Bos-project hebben we een selectie gemaakt van die interfaces die we missiekritiek achtten. Die interfaces hebben we vervolgens in vrij veel detail gemodelleerd en geverifieerd op afwezigheid van deadlocks, livelocks en ongeldige toestanden. Daarnaast hebben we het totale systeem op hoog niveau gemodelleerd met een grote mate van abstractie. Dankzij deze modelverificatie is in een vroeg stadium een fout aan het licht gekomen in het protocol voor de aansturing van de deuren. In uitzonderlijke gevallen zou er bij sluiting van de kering een open kunnen blijven. De kans dat we deze fout tijdens tests zouden hebben gevonden, is miniem. De gevolgen tijdens een stormsituatie zouden desastreus zijn.

De introductie van formele methodes was een flinke investering voor het project. Hoewel modelcheckers voor Promela en Z gratis beschikbaar zijn, hebben de tools en talen een lange inleertijd. Zonder hulp van buiten (in dit geval de UT) zouden we dat niet van de grond hebben gekregen. Het leren van formele methodes loonde voor het Bos-project omdat dat voldoende groot was: 25 manjaar en een doorlooptijd van bijna drie jaar. Uiteindelijk hebben we circa tweeduizend regels Promela en twintigduizend regels Z geschreven en aan de hand daarvan zeshonderdduizend regels C++ geproduceerd. De omzetting van Z naar C++ was een handmatige klus, maar dankzij strikte vertaalrichtlijnen wel een heel eenduidige. In de resulterende code hebben we bijzonder weinig fouten aangetroffen.

Raceconditie

Bij een kleiner project loont het vaak niet om de kennis zelf op te bouwen en is het verstandiger om de formele modelverificatie uit te besteden. Voor deze keuze kwamen we te staan toen we in 2000 voor Rijkswaterstaat een nieuw noodsluitsysteem mochten ontwikkelen voor de Oosterscheldekering, de Noodsluit- en Startautomaat (NSTA). We hadden de kennis van Promela en Z inmiddels in huis en daarmee hebben we het grootste deel van het systeem gemodelleerd.

Op één punt schoten deze formele talen echter tekort: de synchronisatie van de twee redundante systeemhelften. Om aan te tonen dat bij falen van één helft het overschakelen naar de andere helft altijd correct zou verlopen, was een formele verificatie nodig. Helaas bleek Promela niet goed om te kunnen gaan met tijdsafhankelijk gedrag. Daarom zijn we hiervoor uitgeweken naar een andere modelleertaal: Uppaal. De verificatie van dit onderdeel hebben we in zijn geheel uitbesteed aan de UT.

De analyse met Uppaal toonde aan dat de ontwerpers de time-outwaarde om van de ene component naar de andere over te schakelen te laag hadden genomen. De gekozen waarde zou een raceconditie kunnen veroorzaken die in de praktijk bijzonder moeilijk te traceren zou zijn geweest. Daarmee hadden we een mogelijk fatale fout gevonden in de ontwerpfase. Als deze tijdens een acceptatietest of – erger nog – tijdens productie zou zijn opgetreden, dan zou dat tot zeer veel kosten en mogelijk schade hebben geleid.

Overflow

Zonder hulp van een technische universiteit zouden we niet in staat zijn geweest om formele modelverificatie uit te voeren bij de Maeslant- en Oosterschelde-projecten. De Analytical Software Design-methode (ASD) van Verum probeert hier wat aan te doen. Het unieke van ASD is dat de mathematische complexiteit voor de gebruiker verborgen blijft. De methode vereist dat in een tabelvorm voor alle mogelijke toestanden en voor iedere mogelijke input of trigger wordt aangegeven wat de volgende toestand van het systeem zal zijn. Bovendien dwingt ASD de gebruiker daarbij te verwijzen naar de eis die ten grondslag ligt aan de toestandsovergang. Dit brengt al in een vroeg stadium tekortkomingen in de eisen aan het licht.

Een bijkomend voordeel is dat ASD naast een modelchecker ook een codegenerator heeft, die het model rechtstreeks naar C, C++ of C# kan vertalen. Afhankelijk van de toepassing is hiermee 90 procent van de broncode te genereren. Een tijdrovende handmatige omzetting van model naar code, zoals we bij het Bos en de NSTA hebben uitgevoerd, is dan niet meer nodig. Dat scheelt tijd en de code is bovendien gegarandeerd foutvrij.

Bij een treinvolgsysteem, dat Logica ontwikkelt in opdracht van een railbedrijf, hebben we ASD losgelaten op een interface voor informatieoverdracht naar eenzelfde systeem in de buurt. Dit uitwisselingsprotocol hebben we in nauwe samenwerking met Verum gemodelleerd en geverifieerd voor twee treinvolgsystemen en hun interface. Ook hier ontkwamen we er niet aan een vereenvoudiging aan te brengen om het model verifieerbaar te maken. Zonder veel in technische details te treden, zal ik onze oplossing hier beschrijven, omdat het probleem kenmerkend is voor het soort obstakels dat verificatie van modellen opwerpt.

Het binnenkomen van een overdrachtsbericht is voor het model een spontane gebeurtenis; het is op geen enkele manier gerelateerd aan de toestand waarin het treinvolgsysteem zich bevindt en dus onvoorspelbaar. De ASD-modelchecker verifieert vervolgens de situatie waarin oneindig veel berichten oneindig snel na elkaar binnenkomen. Dit leidde in het model tot een overflow van de berichtenbuffer, omdat het systeem de stroom niet snel genoeg zou kunnen verwerken. In de praktijk doet dit zich echter niet voor, want er zullen nooit zo veel treinen tegelijk rijden. Door de gefundeerde aanname te doen dat het systeem altijd voldoende tijd heeft om een bericht te verwerken voordat een volgende overdracht komt, konden we deze situatie omzeilen. De verificatie heeft aangetoond dat het protocol robuust is en niet in een deadlock- of livelocksituatie terecht kan komen. Met andere woorden: het systeem zal nooit blijven ’hangen‘.

Opportuun

De drempel om te beginnen met formele modelverificatie is hoog, maar goed te nemen met hulp van een partij die daar ervaring in heeft. Als we een formele methode eenmaal onder de knie hebben, blijkt de grootste uitdaging te liggen in de modellering. Welke delen gaan we modelleren en in welke mate van detail? Abstraheren maakt dat de focus van een model op hooguit enkele belangrijke aspecten komt te liggen.

In sommige domeinen is het grootste deel van de relevante aspecten te vangen in een enkel model. Dit zijn de gebieden waar codegeneratie opportuun is. ASD is bijvoorbeeld bijzonder geschikt voor het modelleren van controlsoftware en kan in zulke gevallen tot 90 procent van de code genereren. In andere domeinen moeten we zoeken naar combinaties van talen en tools, zoals Promela voor gedrag en Z voor data-integriteit. In die gevallen zal codegeneratie niet mogelijk zijn, maar levert het ontwerp wel een basis voor betrouwbare software, mits de vertaling van ontwerp naar software eenduidig is.

Of we het nu zelf doen of uitbesteden, de kosten van formele modelverificatie verdienen zich dik terug in het testtraject en in de nazorg. Systemen die op deze wijze zijn ontwikkeld, blijken zeer betrouwbaar.