Les langages dédiés de modélisation (DSMLs) sont de plus en plus utilisés dans les phases amont du développement des systèmes complexes, en particulier pour les systèmes critiques embarqués. L’objectif est de pouvoir raisonner très tôt dans le développement sur ces modèles et, notamment, de conduire des activités de vérification et validation (V and V). Une technique très utilisée est la vérification des modèles comportementaux par exploration exhaustive (model-checking) en utilisant une sémantique de traduction pour construire un modèle formel à partir des modèles métiers pour réutiliser les outils performants disponibles pour les modèles formels. Définir cette sémantique de traduction, exprimer les propriétés formelles à vérifier et analyser les résultats nécessite une expertise dans les méthodes formelles qui freine leur adoption et peut rebuter les concepteurs. Il est donc nécessaire de construire pour chaque DSML, une chaîne d’outils qui masque les aspects formels aux utilisateurs. L’objectif de cette thèse est de faciliter le développement de telles chaînes de vérification. Notre contribution inclut 1) l’expression des propriétés comportementales au niveau métier en s’appuyant sur TOCL (Temporal Object Constraint Language), une extension temporelle du langage OCL; 2) la transformation automatique de ces propriétés en propriétés formelles en réutilisant les éléments clés de la sémantique de traduction; 3) la remontée des résultats de vérification grâce à une transformation d’ordre supérieur et un langage de description de correspondance entre le domaine métier et le domaine formel et 4) le processus associé de mise en oeuvre. Notre approche a été validée par l’expérimentation sur un sous-ensemble du langage de modélisation de processus de développement SPEM, et sur le langage de commande d’automates programmables Ladder Diagram, ainsi que par l’intégration d’un langage formel intermédiaire (FIACRE) dans la chaîne outillée de vérification. Ce dernier point permet de réduire l’écart sémantique entre les DSMLs et les domaines formels. / Domain specific Modeling Languages (DSMLs) are increasingly used at the early phases in the development of complex systems, in particular, for safety critical systems. The goal is to be able to reason early in the development on these models and, in particular, to fulfill verification and validation activities (V and V). A widely used technique is the exhaustive behavioral model verification using model-checking by providing a translational semantics to build a formal model from DSML conforming models in order to reuse powerful tools available for this formal domain. Defining a translational semantics, expressing formal properties to be assessed and analysing such verification results require such an expertise in formal methods that it restricts their adoption and may discourage the designers. It is thus necessary to build for each DSML, a toolchain which hides formal aspects for DSML end-users. The goal of this thesis consists in easing the development of such verification toolchains. Our contribution includes 1) expressing behavioral properties in the DSML level by relying on TOCL (Temporal Object Constraint Language), a temporal extension of OCL; 2) An automated transformation of these properties on formal properties while reusing the key elements of the translational semantics; 3) the feedback of verification results thanks to a higher-order transformation and a language which defines mappings between DSML and formal levels; 4) the associated process implementation. Our approach was validated by the experimentation on a subset of the development process modeling language SPEM, and on Ladder Diagram language used to specify programmable logic controllers (PLCs), and by the integration of a formal intermediate language (FIACRE) in the verification toolchain. This last point allows to reduce the semantic gap between DSMLs and formal domains.

De nombreux systèmes hétérogènes sont complexes et critiques. Ces systèmes intègrent du logiciel et des composants matériels avec des interactions fortes entre ces composants. Dans ce contexte, il est devenu absolument nécessaire de développer des méthodologies et des techniques pour spéciier et valider ces systèmes.Dans l'ingénierie des systèmes, les exigences sont l'expression des besoins qu'un produit spécifique ou un service doit réaliser. Elles sont définies formellement à de nombreuses occasions dans l'ingénierie des systèmes complexes. Dans ce type de système, deux catégories d'exigence sont présentes : les exigences non-fonctionnelles telles que la performance et la fiabilité, les exigences fonctionnelles telles que la vivacité. Pour valider ces exigences, un environnement permettant de simuler et vérifier ces propriétés est essentiel.Dans notre travail, nous proposons une méthodologie basée sur SysML et combinée avec SystemC et Promela/SPIN pour spéciier et valider des systèmes complexes. Cette approche est basée sur l'ingénierie dirigée par les modèles pour premièrement traduire des modèles SysML en SystemC afin de réaliser des simulations et deuxièmement traduire des diagrammes d'état SysML en Promela/SPINain de vérifier des propriétés temporelles extraites des exigences. Cette approche est expérimentée sur une étude de cas pour démontrer sa faisabilité. / Heterogeneous Systems are complex and become very critical. These systems integrate software andhardware components with intensive interaction between them. In this context, there is a strongnecessity to develop methodologies and techniques to specify and validate these systems.In engineering, the requirements are the expression of needs on what a particular product or a serviceshould be or to make. They are used most of the time in a formal sense in the systems engineering.In this kind of systems, several types of requirements are present: non-functional requirements suchas the performance and the reliability and functional requirements such as the liveliness. To validatethese requirements of a system, an environment to simulate and to check the properties is essential.In our work, we propose a methodology based on SysML combined with SystemC and Promela/SPINto specify and validate complex systems. This approach is based on Model Driven Engineeringtechniques to irstly translate SysML models to systemC with the aim of simulation and to mapSysML behavioral diagrams to Promela/SPIN in order to verify temporal properties extracted fromthe requirements. The approach is experimented on case studies to demonstrate its feasibility.

Dans cette thèse, nous nous sommes intéressés à l’ouverture des EIAH (EnvironnementsInformatiques pour l'Apprentissage Humain), pour répondre à leur faible déploiement dansles établissements de formation, en facilitant leur appropriation par des usagers. Notre travailde recherche s'inscrit dans le cadre du projet REDiM (Réingénierie des EIAH Dirigée par lesModèles) mené au LIUM (Laboratoire d'Informatique de l'Université du Maine), dont un desobjectifs est d’intégrer les enseignants dans le processus de conception des scénariospédagogiques d’un EIAH.Nous proposons une approche d’ingénierie et de réingénierie pour rendre un EIAH ouvertà la conception et à l’adaptation de ses scénarios pédagogiques par les enseignantsutilisateurs. Nous avons défini un processus de conception basé sur la modélisationde scénarios pédagogiques ouverts (SPO), qui permet l’instrumentation des enseignantspour les aider dans la conception continue (i.e. qui se poursuit dans l’usage) d’une activitéd’apprentissage. Nous faisons trois propositions scientifiques :- Un modèle de représentation des SPO, qui permet de les structurer en variantes enfonction des contextes d’exécution. Nous qualifions ce modèle de rationnel puisqu’il s’appuieprincipalement sur l’approche du Design Rationale que nous avons adaptée à notreproblématique.- Un processus itératif et incrémental d’ingénierie et de réingénierie qui guide lesenseignants pour concevoir et adapter des SPO conformes au modèle que nous avonsdéfini.- Une méthode dirigée par les modèles et spécifique au domaine métier pour instrumenterle processus d’ouverture des scénarios pédagogiques d’un EIAH existant. Cette méthoded’instrumentation, reposant sur l’IDM (Ingénierie Dirigée par les Modèles) et le DSM(Domain-Specific Modeling), implique les enseignants utilisateurs de l’EIAH, considérés icicomme des experts du domaine. Elle est structurée en plusieurs phases qui amènentprogressivement à définir, de façon spécifique à l’EIAH considéré, un langage d’expressiondes SPO (ADSGEML - Adaptive Domain-Specific Graphical Educational ModelingLanguage) et un éditeur associé permettant la conception et l’adaptation des SPO dansl’univers métier de l’EIAH.Afin d’évaluer et de raffiner nos propositions, nous les avons appliquées sur l’EIAH«Hop3x», préalablement conçu au LIUM dans le cadre d’un autre projet pour pratiquer laprogrammation orientée objet. Nous avons donc élaboré un ADSGEML et un environnementd’édition graphique pour permettre aux enseignants de concevoir et d’adapterdynamiquement des sessions ouvertes de Hop3x, à un niveau élevé d’abstraction. / In this thesis, we are interested in opening TEL systems (Technology EnhancedLearning) up in order to respond to the problem of their low deployment in teachinginstitutions, we need to facilitate their adoption by users. Our research work is part ofthe REDiM (French abbreviation which means “Model-Driven Re-engineering of TELsystems”) project led by the LIUM Computer Science Laboratory of Le MansUniversity in France. One of the main objectives of this project is to involve teachersin the design process of learning scenarios of a TEL system.We propose an engineering and re-engineering approach for opening TEL systemsin order to facilitate for teachers the design and adaptation of pedagogical scenarios.We defined a design process based on the modeling of Open Pedagogical Scenarios(OPS), which allows the building of supports helping teachers in the continuousdesign of a learning activity (i.e. design which continues in the use process). Wemake three scientific proposals:- A model of OPS representation which defines a structure based on variantsaccording to execution contexts. We consider this model to be “rational” because it isbased mainly on the Design Rationale approach that we have adapted for ourresearch problem.- An iterative and incremental engineering and re-engineering process that guidesteachers to design and adapt OPS according to the rational model that we define inthis work.- A model-driven and domain-specific method for supporting the process of openingpedagogical scenarios of a legacy TEL system. This method, based on the MDE(Model-Driven Engineering) and DSM (Domain-Specific Modelling), involves teachersusing the TEL system, as they are considered to be domain experts. Our method isdivided into several phases that lead progressively to define the TEL system’sADSGEML (Adaptive Educational Graphical Domain-Specific Modelling Language)and an associate editor allowing the design and adaptation of OPS in the businessfield of the TEL system to open for teachers.To evaluate and refine our proposals, we have applied them on the TEL system"Hop3x" which was designed at LIUM under another project for practicing objectorientedprogramming. We therefore developed an ADSGEML and a graphicalediting environment to enable teachers to design and adapt dynamically the openHop3x’s learning sessions at a high level of abstraction.