Formal alignment of requirements models with high-level architecture models

The quality of a system depends on the degree to which it fulfills its requirements. Requirements traceability is broadly recognized as a crucial element of any rigorous system development process, especially for the design of critical complex systems. The paper proposes a model-based approach to support traceability by defining several kinds of alignment links between requirements models and high-level architecture models. We have already defined these models using a combination of graphical notations based on SysML and the formal method Event-B, hence alignment links are first graphically specified by refining the Dependency concept of SysML. Then they are translated into Event-B specifications. The main idea is to use the formal refinement concept to prove their correctness. As the semantics of this refinement is not the same as the standard Event-B refinement, we have defined new proof obligations to express it, which can be discharged using Atelier B. Finally we illustrate our approach on a case study from the railway domain.