UML/B modeling for the safety requirements validation of railway operating rules

La sécurité est un enjeu majeur dans le cycle de développement des systèmes critiques, notamment dans le secteur du transport ferroviaire. Cette thèse vise la modélisation, la vérification et la validation des règles d'exploitation ferroviaires au regard des exigences de sécurité. Ces règles ont pour but de définir les autorisations de déplacement des trains sur des lignes ferroviaires nationales équipées du système européen de gestion du trafic ferroviaire (ERTMS). De manière analogue, on trouve les concepts liés aux autorisations dans la description des politiques de contrôle d'accès des systèmes d'information. Par conséquent, nos contributions portent sur l'adaptation d'une approche UML/B pour le contrôle d'accès des systèmes d'information afin de modéliser et de valider les règles d'exploitation ferroviaires. Dans un premier temps, nous avons adapté le modèle Role Based Access Control (RBAC) sur une étude de cas ferroviaire extraite des règles d'exploitation appliquées sur la ligne à grande vitesse LGV Est-Européenne en France. La plate-forme B4MSecure nous a permis de modéliser ces règles à l'aide d'un profil UML de RBAC inspiré de SecureUML. Ensuite, ces modèles sont transformés en des spécifications B qui ont été enrichies par des propriétés de sécurité ferroviaire et soumises à des activités de vérification et de validation formelles. Aux concepts du modèle RBAC, le modèle Organization Based Access Control (Or-Bac) introduit la notion d'organisation, au centre de ce modèle, et la notion de contexte. Nous avons donc proposé d’utiliser ce modèle en tant qu’extension du modèle RBAC dans l’optique d’une interopérabilité ferroviaire en ERTMS.The safety is a major issue in the development cycle of the critical systems, in particular in the rail transportation sector. This thesis aims at the modeling, the verification and at the validation of the railway operating rules with regard to the safety requirements. These rules intend to define the authorizations of trains movement on national railway lines equipped with the European Rail Traffic Management System (ERTMS). In a similar way, we find the concepts of authorizations in the description of access control policies of information systems. Consequently, our contributions concern the adaptation of an UML/B approach for the access control of information systems to model and validate the railway operating rules. At first, we adapted the Role Based Access Control (RBAC) model on a railway case study extracted from the operating rules applied on the LGV-Est-Européenne line in France. The B4MSecure platform enables the modeling of these rules by means of a UML profile of RBAC inspired by SecureUML. Then, these models are transformed into B specifications. which are enhanced by railway safety properties and formally verified and validated. In addition to the concepts of the RBAC model, the Organization Based Access Control (Or-Bac) model introduces the notion of organization, in the center of this model, and the notion of context. We have therefore proposed to use this model as extension of the RBAC model in the context of railway interoperability in ERTMS