Willem Rietdijk: Compositional verification of control software UML models


Event Details


Abstract: Low Code Development Platforms, such as the Cordis SUITE, facilitate formal verification in software development for industrial automation. An automated translation from Cordis models to mCRL2 enables the for-
mal verification of real-world industry models. However, this approach is not without challenges. The monolithic nature of the translation can lead to state space explosions in larger models. Compositional verification
methods aim to mitigate state space explosion by separately generating components and applying reduction techniques before they are composed. In this thesis, we apply compositional verification to Cordis models and evaluate various techniques designed to increase our ability to perform verification of larger models. Our findings show that compositional verification significantly reduces state space explosion. However, in its current form, it is not yet the be-all and end-all solution to the problem. The inherent cyclic behavior of Cordis models present notable difficulties that are not easily overcome.

We demonstrate the application of our compositional verification approach by assessing a set of requirements on a model of the Bosrandbrug. This assessment uncovers minor defects within the model, which can be
rectified with straightforward modifications.