Towards the Strengthening of Capella Modeling Semantics by Integrating Event-B: A Rigorous Model-Based Approach for Safety-Critical Systems

Safety-critical systems are increasingly model-based, since model-based system engineering (MBSE) paradigm reduces the time-to-market and allows evolving systems at different abstraction levels. Different languages have been proposed recently enabling to facilitate the modeling process and shorten the development life-cycle. However, these languages may be used at one or many modeling steps regarding the semantics of their artefacts. Capella language is one of these languages that gained popularity recently. It is dedicated to system engineering and its use may very beneficial for safety-critical system. However, designing with Capella is considered as semi-formal. Thus, the approach presented in this paper stands for systematic formal verification of Capella’s behavioral models using Event-B method in a transparent way. Our proposal translates Capella models into Event-B specifications using automatic model-to-model transformations dedicated to Capella designers. The verification of correctness of the transformed models is provided by the ProB model-checker. An automatic lighting system is treated as a case study to validate of our contribution.