This thesis presents the light signal case study as part of the FormaSig project, which aims to use formal methods to support the development of EULYNX – a European initiative to standardise interfaces of signalling systems. EULYNX specifies its interfaces using SysML, which is a semi-formal modelling language. Previous research has developed a formalisation for auto-translating these SysML models to mCRL2. The first goal is to verify the SysML models of the light signal interface in mCRL2 by interpreting the SysML models directly instead of using automatic translation. The second goal is to perform a comparative study between the hand-made and the auto-translated model. The formalisation is made for all SysML models and hence has to include all SysML aspects, which can lead to enormous state space of billions of states. A case study has been executed on a smaller system – the point, which already has 5.14 · 10^10 states because of the formalisation. Hence, the auto-translated model for the light signal system might become too big for model-checking since the light signal system is larger than the point system.

The main idea behind this project is to look into the choices made for modelling and see whether these choices lead to meaningful verification of the specification and inspire improvements in the automated translation process. These improvements can then lead to improved models for the FormaSig project. An mCRL2 model is created and verified while keeping track of the choices made in the modelling process. At the end of this research, the models are checked against the specified requirements, which leads to confirming found problems in the specification. Furthermore, a comparative study between the models is executed in terms of usability, which shows a trade-off between maintainability and verifiability.