Wanneer TU/e-informaticus Mark Bouwman in de trein zit – en dat is best vaak, hij heeft bewust geen auto – wordt zijn aandacht bijna automatisch richting spoorberm getrokken. De diverse kastjes langs de rails hebben na jaren onderzoek weinig geheimen meer voor hem. In een onderzoeksconsortium met Universiteit Twente en spoorwegmaatschappijen ProRail en Deutsche Bahn bekeek Bouwman hoe er voor de aansturing van seinen en wissels veilig naar een nieuw communicatiesysteem overgestapt kan worden. Maandag 23 oktober verdedigt hij zijn promotieonderzoek aan de faculteit Mathematics and Computer Science.

Sein op rood

Zie je nu een sein op rood springen, dan wordt deze aangestuurd door een centrale computer – in vaktermen de interlocking – via een directe kabel, legt Bouwman uit. “De interlocking zorgt ervoor dat treinen niet botsen. Elk Europees station heeft zijn eigen interlocking met in de basis hetzelfde aansturingsprincipe. Maar toch zijn ze allemaal net iets anders. En daar willen de Europese spoorwegmaatschappijen vanaf. Over een aantal jaar moeten de veldelementen binnen Europa door hetzelfde protocol worden aangestuurd.”

Er wordt daarom overgestapt naar een andere manier van communiceren. Niet meer via een directe kabel, maar met een glasvezelnetwerk. Zo moet de interlocking dan pakketjes informatie aan een specifiek sein kunnen adresseren: je gaat nu op rood. Dat dat systeem binnen Europa hetzelfde gaat worden, heeft volgens Bouwman meerdere voordelen. “De apparatuurmarkt wordt ineens veel groter. Een Nederlands sein kan dan ook in andere landen gebruikt worden, wij kunnen gebruik maken van buitenlandse wissels. Innovaties komen zo sneller op de markt. En door het gebruik van een glasvezelnetwerk is het geheel minder gevoelig voor kabelbreuken. Gaat er nu bij graafwerkzaamheden een kabel door dan resulteert dat in een seinstoring, met alle ellende van dien. Een glasvezelnetwerk is veel flexibeler zodat er eenvoudiger signaal-omleidingen kunnen worden gemaakt. En qua duurzaamheid is het ook fijn dat interlocking en bedrading losgekoppeld worden, nu moet altijd het geheel vervangen worden.”

Steentje tussen de wissel

Veel voordelen dus. Maar voordat er gewerkt kan worden met een nieuwe communicatiestandaard, moet de veiligheid tot in het miniemste detail gegarandeerd zijn. En daar kwam de wiskunde van Bouwman bij van pas. “Door een protocol logisch te specificeren ga je alle mogelijkheden na waardoor je precies weet hoe het werkt en kun je een systeem zo dichttimmeren.” Voor deze stap-voor-stap aanpak had Bouwman een hele toolkit tot zijn beschikking, zoals de aan de TU/e ontwikkelde modelleertaal mCLR2. “Die herprogrammering is heel belangrijk. Als je iets opschrijft in gewone taal, kun je te maken krijgen met ambiguïteiten. Maar in dit geval moet het zo eenduidig mogelijk zijn. Daarna konden we gaan doorrekenen wat al het mogelijke gedrag van het systeem zou kunnen zijn. Een wissel kan op het juiste moment omspringen, maar er kan ook een steentje klem zitten, of iemand zet er een koevoet tussen. Je doet geen aannames, maar beschrijft alle toestanden waarin het terecht kan komen.”

Supercomputer

Om specificaties efficiënt om te zetten naar mCLR2-taal zette Bouwman een nieuw systeem op. Een hele uitdaging waar veel rekenkracht voor nodig was, legt hij uit. “Je moet miljoenen, miljarden toestanden doorrekenen, dat zijn al die paden waarin het systeem zich ooit zou kunnen bevinden. Binnen onze vakgroep gebruiken we de Mastodont, een supercomputer waar we alle complexe berekeningen mee kunnen doen. Maar omdat de toestandsruimte – alle mogelijkheden en paden daartussen – ondertussen zo groot was geworden had, liep ook de Mastodont daar op vast.”