Lessons Learned/Sharing the Experience of Developing a Metro System Case Study
This is an incremental contribution sharing practical experiences for developers and researchers in formal methods and system modeling.
The authors tackled the challenge of modeling a large metro system by developing a case study using Event-B and the Rodin platform, identifying key modeling techniques and tool strengths/weaknesses through stepwise refinement from requirements.
In this document we share the experiences gained throughout the development of a metro system case study. The model is constructed in Event-B using its respective tool set, the Rodin platform. Starting from requirements, adding more details to the model in a stepwise manner through refinement, we identify some keys points and available plugins necessary for modelling large systems (requirement engineering, decomposition, generic instantiation, among others), which ones are lacking plus strengths and weaknesses of the tool.