Many large infrastructure systems, such as bridges, tunnels, sluices and floodgates, were built in an era when digital modelling and mathematical analysis either did not exist or were considered purely theoretical concepts. Rijkswaterstaat is now exploring how the benefits of formal, model-based approaches can be applied to develop working control system models of the assets in its portfolio. The goal is to ensure their sustainable maintenance for the duration of their expected lifespan, which is often 50 years or more.
Over the past years, Jan Friso Groote, full Professor of Formal System Analysis at Eindhoven University of Technology, was responsible for modelling the control software of the Maeslant kering. This is the largest and most complex system of them all. On behalf of Rijkswaterstaat, Programme Manager Yigal Levin acted as his counterpart. Both agree that the fusion of in-depth domain knowledge with formal modelling expertise is essential for the success of such projects. Groote wishes to make one thing crystal clear up-front: ‘We are not talking about a simplified version of a partial model of an object here. This is about a model describing the complete control software with all of its real-world functions.’ Two challenges stand out during the execution of such a project, he says: ‘It is very hard to find out what software in actual systems is doing, or is supposed to do precisely. But if you make a formal model, you have to know. I have seen many people trying this for systems far less complex than the Maeslantkering, who gave up. But not in this case. With the excellent support of Rijkswaterstaat, we managed to produce the precise model.’
This typically regards questions about detail, such as: ‘You are supposed to push this lever once. But what happens when you push it twice or three times?’ This requires sharpness from the modeller and answers that even the experts have not always thought about, because you are not supposed to do it. Groote: ‘But since it can happen, you have to think about it. As a modeller, you should not seek the solution by yourself, but follow the thinking of the object expert in a dialogue. That is the first challenge.’
Size of the models
The second challenge is related to the limits of the “human condition”. Groote: ‘We need to describe a system integrally and correctly – but we know that we as humans make errors while doing this. A plus sign is easily switched for a minus sign when it is close to cup-a-soup time. We therefore have to verify the entire model in all its behavioural characteristics in all pos sible variants.’ But this verification is hard because the models are big. There are only 1080 atoms in the universe. ‘However, the number of different situations a software controller, such as for a railway network or a tunnel, can be in can easily exceed 101000, says Groote. It is hard to wrap your head around that. ‘If the model contains too many of these situations, which we call states, ‘It is very hard to find out what software in actual systems is doing, or is supposed to do precisely. But if you make a formal model, you have to know’ then it becomes impossible to verify all states. Therefore, we need to make a model restricting the number of states, with out compromising the principle of simplifying the model com pared to reality. For instance, there should be no shenanigans when modelling malfunctions of sensors and actuators. We managed to do this with the Maeslantkering. When we math ematically analysed the behaviour of the model, it outwitted the experts. This built trust in the model.’
Sustainably maintainable
Yigal Levin, Programme Manager at Rijkswaterstaat, explains the rationale behind the effort: ‘We need to be able to trust that the assets we manage behave exactly as they were designed to without surprises. Most of the tunnels, bridges, and sluices under our responsibility were built between the 1950s and 1980s. Their physical structures were designed in a highly structured way, based on clear calculations of struc tural strength; something you can still verify in the technical drawings. The digital control systems of these complex assets should be designed just as systematically. But with legacy ICT systems, it’s very difficult to demonstrate this in retrospect. This calls for ongoing professionalisation.’ ‘To catch up, we’re now building that proof using formal models developed by highly experienced institutions such as Eindhoven University of Technology and the University of Twente.
This approach helps us prepare for future developments by making our systems future-proof and sustainably maintainable.’ A crucial aspect for successful modelling is the collaboration between the genuine domain experts of the asset manage ment organisation and the ICT specialists of the contractor. Groote: ‘As accuracy is vital, interpretation must be ruled out as much as possible. Ultimately, you have the back-end veri f ication tool mCRL2 to prove the validity, but effective com munication with the right level of Rijkswaterstaat domain experts helped to prevent misunderstandings and thus to work efficiently. I have great appreciation for the fact that Rijkswaterstaat understood how important it is to spare their scarce domain experts for this project. Not every organisation understands how vital that is.’ Levin adds: ‘Our collaboration has been very productive indeed, also thanks to the knowledge level and methods applied by the researchers in the project. The model proved to be nearly 100 percent correct right away. Reliable models like these are vital for our future as an asset manager.’
Integral model
The same approach is also applicable for other assets within Rijkswaterstaat, such as sluices, bridges and tunnels, but also for systems outside the organisation, Levin emphasises, such as railway networks or nuclear power plants. ‘Having verifiable models creates peace of mind.’ Groote is also glad that a com plete approach with modelling principles and modelling lan guage is in place, creating models with infinitely more precise language than natural language could ever produce. ‘I must admit that the integral model we have now is something of a surprise even to me.’ ‘Many projects of this type get stuck halfway’, he says. ‘The ambitions are then tuned down, for instance, to the creation of a partial model. No such thing is happening here: we have modelled the entire Maeslantkering, with opening and closure processes true to nature. That is no trivial feat, given the com plex interaction of the Maeslantkering itself with the weather and hydrology dynamics at large. All things considered, this is an achievement we can rightly be proud of.’
By Leendert van der Ent
Images WAT ontwerpers, iStock