Dans le monde des systèmes qui utilisent des communications sous forme de diffusion de groupes, le critère de sécurité devient un facteur de plus en plus important. Le choix des mécanismes pour la protection de cette communication, mécanismes basés sur des échanges de clés symétriques et asymétriques, influe sur l'efficacité du système. Nous avons procédé à l'analyse des besoins et nous avons défini un modèle qui permet de représenter la dynamique des groupes et la communication entre leurs membres. Nous avons défini l'architecture d'un système dont l'élément central est la fonction de création, d'échange et de mise en place correcte des clés. La modélisation de ce système dans un environnement UML 2.0 a permis son analyse en termes de garantie de propriétés temporelles et de sécurité. L'approche suivie pour l'étude des exigences temporelles est généralisable à de nombreux systèmes distribués. La valorisation de nos études a été faite dans le cadre du projet national RNRT SAFECAST.

Fortement marqués par les avancées en Génie Logiciel, les travaux présentés dans ce mémoire ont pour objectif de proposer un langage permettant de produire des modèles acceptables d'un EIAH c'est-à-dire dire des modèles dont il est possible d'évaluer la pertinence. Ceci signifie que les modèles sont explicites, non ambigus et qu'ils rendent possible des échanges entre les acteurs de la conception pour faire évoluer des modèles d'un état inaccepté à un état accepté. L'idée est donc de capitaliser sur la base des modèles de conception plutôt que sur le code des EIAH produits. L'explicitation des modèles de conception (théories d'apprentissage sur lesquelles s'appuie l'EIAH à construire, scénarios d'apprentissage et principes d'interaction) doit permettre de mieux partager les expertises au sein des équipes de développement et donc de diffuser les savoirs et bonnes pratiques. Par ailleurs, il s'agit d'examiner les conditions de transformations des modèles de conception en modèles computationnels afin de pouvoir réutiliser / transformer ces modèles vers des modèles exploitables par des plates-formes de formation à distance et faciliter ainsi le travail de mise en œuvre.<br /><br />Dans ce document, je positionne tout d'abord les travaux proposés au sein de la communauté EIAH (chapitre 1) ce qui me permet d'expliciter les théories d'apprentissage auxquelles ces travaux se réfèrent ainsi que les principaux verrous scientifiques posés par l'ingénierie des EIAH. Le chapitre 2 présente ma démarche de recherche au cours de ces travaux ainsi que les questions de recherche spécifiques qui sont au cœur des activités menées. Ce chapitre me permet donc de positionner mes travaux par rapport à ceux que mènent d'autres équipes nationales et internationales sur des problématiques identiques. Je présente ensuite (chapitre 3) les principaux résultats qui portent sur l'ingénierie de modèles de conception pour les situations d'apprentissage de type situations-problèmes coopératives, mais aussi sur l'usage de ces modèles et la démarche de conception qu'ils supposent. Les travaux qui se sont succédés ont permis de définir et d'expérimenter différents langages visuels, ce qui nous a conduit à proposer un profil UML dédié à la description des situations problèmes coopératives, le langage CPM. Le chapitre 4 me permet enfin de dresser un bilan de mon activité d'enseignant chercheur à l'Université de Pau et des Pays de l'Adour.

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.