Although originally designed as an extension for the Unifi ed Modeling Language (UML), today, the Object Constraint Language (OCL) has been broadly adopted in the context of both UML and other modeling and domain-specifi c languages. However, appropriate tooling, supporting modelers and software developers on using OCL is still scarce and lacks important features such as debugging support. As OCL constraints are likely to become rather complex for real world examples, it is hard to comprehend the in uence of single OCL expressions and subexpressions on the result of a completely evaluated OCL constraint in the context of speci fic constrained objects. Therefore, debugging is of topmost importance for both constraint comprehension and maintenance. Thus, the major task of this work is to develop a graphical debugger integrated into Dresden OCL and the Eclipse Integrated Development Environment (IDE) to fill this gap.

Although originally designed as an extension for the Unifi ed Modeling Language (UML), today, the Object Constraint Language (OCL) has been broadly adopted in the context of both UML and other modeling and domain-specifi c languages. However, appropriate tooling, supporting modelers and software developers on using OCL is still scarce and lacks important features such as debugging support. As OCL constraints are likely to become rather complex for real world examples, it is hard to comprehend the in uence of single OCL expressions and subexpressions on the result of a completely evaluated OCL constraint in the context of speci fic constrained objects. Therefore, debugging is of topmost importance for both constraint comprehension and maintenance. Thus, the major task of this work is to develop a graphical debugger integrated into Dresden OCL and the Eclipse Integrated Development Environment (IDE) to fill this gap.:1 Introduction 2 The Dresden OCL Toolkit 2.1 The Dresden OCL Toolkit 2.2 The Dresden OCL2 Toolkit 2.3 Dresden OCL2 for Eclipse 2.4 Dresden OCL 3 The Eclipse Debugging Framework 3.1 The Debug Model 3.2 Interacting with the Debug Model 3.3 The Execution Control Commands 4 Requirements Analysis and Related Work 4.1 Requirements Analysis 4.2 Related Work 5 Design and Structure 5.1 Architecture 5.1.1 Package Structure 5.1.2 Class Structure 5.2 The OCL Debug Model 5.3 The Mapping from ASM to AST 5.4 The OCL Debugger 5.4.1 The Implementation of the Debugger 5.4.2 Testing the Debugger 6 Graphical User Interface Implementation 6.1 The Dresden OCL Debug Perspective 6.2 Using the Debugger 6.2.1 Selecting a Model 6.2.2 Selecting a Model Instance 6.2.3 Debugging 6.3 Summary 7 Evaluation and Future Work 33 7.1 Evaluation 7.2 Future Work 8 Summary and Conclusion

Indiana University-Purdue University Indianapolis (IUPUI) / This thesis investigates integrating recommender systems into model-driven engineering tools powered by domain-specific modeling languages. The objective of integrating recommender systems into such tools is overcome a shortcoming of proactive modeling where the modeler must inform the model intelligence engine how to progress when it cannot automatically determine the next modeling action to execute (e.g., add, delete, or edit). To evaluate our objective, we integrated a recommender system into the Proactive Modeling Engine, which is a add-on for the Generic Modeling Environment (GME). We then conducted experiments to both subjective and objectively evaluate the enhancements to the Proactive Modeling Engine. The results of our experiments show that integrating recommender system into the Proactive Modeling Engine results in an Average Reciprocal Hit-Rank (ARHR) of 0.871. Likewise, the integration results in System Usability Scale (SUS) rating of 77. Finally, user feedback shows that the integration of the recommender system to the Proactive Modeling Engine increases the usability and learnability of domain-speci c modeling tools.

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.

Industries have adopted a standardized set of practices for developing their products. In the automotive domain, the provision of safety-compliant systems is guided by ISO 26262, a standard that specifies a set of requirements and recommendations for developing automotive safety-critical systems. For being in compliance with ISO 26262, the safety lifecycle proposed by the standard must be included in the development process of a vehicle. Besides, a safety case that shows that the system is acceptably safe has to be provided. The provision of a safety case implies the execution of a precise documentation process. This process makes sure that the work products are available and traceable. Further, the documentation management is defined in the standard as a mandatory activity and guidelines are proposed/imposed for its elaboration. It would be appropriate to point out that a well-documented safety lifecycle will provide the necessary inputs for the generation of an ISO 26262-compliant safety case. The OSLC (Open Services for Lifecycle Collaboration) standard and the maturing stack of semantic web technologies represent a promising integration platform for enabling semantic interoperability between the tools involved in the safety lifecycle. Tools for requirements, architecture, development management, among others, are expected to interact and shared data with the help of domains specifications created in OSLC.This thesis proposes the creation of an OSLC tool-chain infrastructure for sharing safety-related information, where fragments of safety information can be generated. The steps carried out during the elaboration of this master thesis consist in the identification, representation, and shaping of the RDF resources needed for the creation of a safety case. The focus of the thesis is limited to a tiny portion of the ISO 26262 left-hand side of the V-model, more exactly part 6 clause 8 of the standard:  Software unit design and implementation. Regardless of the use of a restricted portion of the standard during the execution of this thesis, the findings can be extended to other parts, and the conclusions can be generalize.This master thesis is considered one of the first steps towards the provision of an OSLC-based and ISO 26262-compliant methodological approach for representing and shaping the work products resulting from the execution of the safety lifecycle, documentation required in the conformation of an ISO-compliant safety case. / Espresso 2 / Gen&ReuseSafetyCases

Le raisonnement spatial et temporel qualitatif est un domaine principal d’études de l’intelligence artificielle et, en particulier, du domaine de la représentation des connaissances, qui traite des concepts cognitifs fondamentaux de l’espace et du temps de manière abstraite. Dans notre thèse, nous nous focalisons sur les formalismes du domaine du raisonnement spatial et temporel qualitatif représentant les informations par des contraintes et apportons des contributions sur plusieurs aspects. En particulier, étant donnée des bases de connaissances d’informations qualitatives sur l’espace ou le temps, nous définissons des nouvelles conditions de consistance locale et des techniques associées afin de résoudre efficacement les problèmes fondamentaux se posant. Nous traitons notamment du problème de la satisfiabilité qui est le problème de décider s’il existe une interprétation quantitative de toutes les entités satisfaisant l’ensemble des contraintes qualitatives. Nous considérons également le problème de l’étiquetage minimal qui consiste à déterminer pour toutes les contraintes qualitatives les relations de base participant à au moins une solution ainsi que le problème de redondance consistant à déterminer les contraintes qualitatives non redondantes. En outre, nous enrichissons le domaine des formalismes spatio-temporels par des contributions concernant une logique spatio-temporelle combinant la logique temporelle propositionnelle (PTL) avec un langage de contraintes qualitatives spatiales et une étude de la problématique consistant à gérer une séquence temporelle de configurations spatiales qualitatives devant satisfaire des contraintes de transition. / Qualitative Spatial and Temporal Reasoning is a major field of study in Artificial Intelligence and, particularly, in Knowledge Representation, which deals with the fundamental cognitive concepts of space and time in an abstract manner. In our thesis, we focus on qualitative constraint-based spatial and temporal formalisms and make contributions to several aspects. In particular, given a knowledge base of qualitative spatial or temporal information, we define novel local consistency conditions and related techniques to efficiently solve the fundamental reasoning problems that are associated with such knowledge bases. These reasoning problems consist of the satisfiability problem, which is the problem of deciding whether there exists a quantitative interpretation of all the entities of a knowledge base such that all of its qualitative relations are satisfied by that interpretation, the minimal labeling problem, which is the problem of determining all the atoms for each of the qualitative relations of a knowledge base that participate in at least one of its solutions, and the redundancy problem, which is the problem of obtaining all the non-redundant qualitative relations of a knowledge base. Further, we enrich the field of spatio-temporal formalisms that combine space and time in an interrelated manner by making contributions with respect to a qualitative spatio-temporal logic that results by combining the propositional temporal logic (PTL) with a qualitative spatial constraint language, and by investigating the task of ordering a temporal sequence of qualitative spatial configurations to meet certain transition constraints.

Les systèmes d'Entrepôts de Données et OLAP spatiaux (EDS et SOLAP) sont des technologies d'aide à la décision permettant l'analyse multidimensionnelle de gros volumes de données spatiales. Dans ces systèmes, la qualité de l'analyse dépend de trois facteurs : la qualité des données entreposées, la qualité des agrégations et la qualité de l’exploration des données. La qualité des données entreposées dépend de critères comme la précision, l'exhaustivité et la cohérence logique. La qualité d'agrégation dépend de problèmes structurels (e.g. les hiérarchies non strictes qui peuvent engendrer le comptage en double des mesures) et de problèmes sémantiques (e.g. agréger les valeurs de température par la fonction Sum peut ne pas avoir de sens considérant une application donnée). La qualité d'exploration est essentiellement affectée par des requêtes utilisateur inconsistantes (e.g. quelles ont été les valeurs de température en URSS en 2010 ?). Ces requêtes peuvent engendrer des interprétations erronées des résultats. Cette thèse s'attaque aux problèmes d'incohérence logique qui peuvent affecter les qualités de données, d'agrégation et d'exploration. L'incohérence logique est définie habituellement comme la présence de contradictions dans les données. Elle est typiquement contrôlée au moyen de Contraintes d'Intégrité (CI). Dans cette thèse nous étendons d'abord la notion de CI (dans le contexte des systèmes SOLAP) afin de prendre en compte les incohérences relatives aux agrégations et requêtes utilisateur. Pour pallier les limitations des approches existantes concernant la définition des CI SOLAP, nous proposons un Framework basé sur les langages standards UML et OCL. Ce Framework permet la spécification conceptuelle et indépendante des plates-formes des CI SOLAP et leur implémentation automatisée. Il comporte trois parties : (1) Une classification des CI SOLAP. (2) Un profil UML implémenté dans l'AGL MagicDraw, permettant la représentation conceptuelle des modèles des systèmes SOLAP et de leurs CI. (3) Une implémentation automatique qui est basée sur les générateurs de code Spatial OCL2SQL et UML2MDX qui permet de traduire les spécifications conceptuelles en code au niveau des couches EDS et serveur SOLAP. Enfin, les contributions de cette thèse ont été appliquées dans le cadre de projets nationaux de développement d'applications (S)OLAP pour l'agriculture et l'environnement. / Spatial Data Warehouse (SDW) and Spatial OLAP (SOLAP) systems are Business Intelligence (BI) allowing for interactive multidimensional analysis of huge volumes of spatial data. In such systems the quality ofanalysis mainly depends on three components : the quality of warehoused data, the quality of data aggregation, and the quality of data exploration. The warehoused data quality depends on elements such accuracy, comleteness and logical consistency. The data aggregation quality is affected by structural problems (e.g., non-strict dimension hierarchies that may cause double-counting of measure values) and semantic problems (e.g., summing temperature values does not make sens in many applications). The data exploration quality is mainly affected by inconsistent user queries (e.g., what are temperature values in USSR in 2010?) leading to possibly meaningless interpretations of query results. This thesis address the problems of logical inconsistency that may affect the data, aggregation and exploration qualities in SOLAP. The logical inconsistency is usually defined as the presence of incoherencies (contradictions) in data ; It is typically controlled by means of Integrity Constraints (IC). In this thesis, we extends the notion of IC (in the SOLAP domain) in order to take into account aggregation and query incoherencies. To overcome the limitations of existing approaches concerning the definition of SOLAP IC, we propose a framework that is based on the standard languages UML and OCL. Our framework permits a plateforme-independent conceptual design and an automatic implementation of SOLAP IC ; It consists of three parts : (1) A SOLAP IC classification, (2) A UML profile implemented in the CASE tool MagicDraw, allowing for a conceptual design of SOLAP models and their IC, (3) An automatic implementation based on the code generators Spatial OCLSQL and UML2MDX, which allows transforming the conceptual specifications into code. Finally, the contributions of this thesis have been experimented and validated in the context of French national projetcts aimming at developping (S)OLAP applications for agriculture and environment.

Dans l’industrie de l’avionique, les Générateurs Automatiques de Code (GAC) sont de plus en plus utilisés pour produire des parties du logiciel embarqué. Puisque le code généré fait partie d’un logiciel critique, les standards de sûreté exigent une vérification approfondie du GAC: la qualification. Dans cette thèse en collaboration avec AdaCore, nous cherchons à réduire le coût des activités de test par des méthodes automatiques et efficaces.La première partie de la thèse aborde le sujet du test unitaire qui assure une exhaustivité élevée mais qui est difficile à réaliser pour les GACs. Nous proposons alors une méthode qui garantit le même niveau d’exhaustivité en n’utilisant que des tests d’intégration de mise en œuvre plus facile. Nous proposons tout d’abord une formalisation du langage ATL de définition du GAC dans la théorie des Transformations Algébriques de Graphes. Nous définissons ensuite une traduction de postconditions exprimant l’exhaustivité du test unitaire en des préconditions équivalentes qui permettent à terme de produire des tests d’intégration assurant le même niveau d’exhaustivité. Enfin, nous proposons d’optimiser l’algorithme complexe de notre analyse à l’aide de stratégies de simplification dont nous mesurons expérimentalement l’efficacité.La seconde partie du travail concerne les oracles de tests du GAC, c’est à dire le moyen de valider le code généré par le GAC lors d’un test. Nous proposons un langage de spécification de contraintes textuelles capables d’attester automatiquement de la validité du code généré. Cette approche est déployée expérimentalement à AdaCore pour le projet QGen, un générateur de code Ada/C à partir de Simulink®. / In the avionics industry, Automatic Code Generators (ACG) are increasingly used to produce parts of the embedded software. Since the generated code is part of critical software, safety standards require a thorough verification of the ACG called qualification. In this thesis in collaboration with AdaCore, we seek to reduce the cost of testing activities by automatic and effective methods.The first part of the thesis addresses the topic of unit testing which ensures exhaustiveness but is difficult to achieve for ACGs. We propose a method that guarantees the same level of exhaustiveness by using only integration tests which are easier to carry out. First, we propose a formalization of the ATL language in which the ACG is defined in the Algebraic Graph Transformation theory. We then define a translation of postconditions expressing the exhaustiveness of unit testing into equivalent preconditions that ultimately support the production of integration tests providing the same level of exhaustiveness. Finally, we propose to optimize the complex algorithm of our analysis using simplification strategies that we assess experimentally.The second part of the work addresses the oracles of ACG tests, i.e. the means of validating the code generated by the ACG during a test. We propose a language for the specification of textual constraints able to automatically check the validity of the generated code. This approach is experimentally deployed at AdaCore for a Simulink® to Ada/C ACG called QGen.