La principale contribution de cette thèse porte sur la proposition et le développement d'une approche d'Ingénierie Dirigée par les Modèles (IDM), liée à une méthodologie basée sur des composants, pour faciliter la conception, design et implantation des Systèmes Dynamiquement Reconfigurables sur puce (FPGA). La méthodologie proposée repose sur l'utilisation du paradigme Metadata-based Composition Framework, et fortement basée sur des standards, tels qu'UML MARTE et, en particulier, l'IEEE IP-XACT, qui est exploitée comme représentation intermédiaire pour les IPs utilisés et pour la plateforme matérielle composée aux hautes-niveaux d'abstraction. Un procès d'emballage permet la réutilisation des bloques IP, qui ont été enveloppés par des interfaces PLB (IP statiques) et propriétaires (IP dynamiques). Subséquemment, la libraire est utilisée pour la composition d'un modèle de plateforme en UML, mais qui étant générative, permet la création d'une description cible de la composante matérielle de la plateforme, dans la forme d'un modèle spécifique à Xilinx Platform Studio, obtenu par des transformations des modèles. Les chaines de transformations pour la création de la libraire et de la plateforme, respectivement, ont été développées et implantées en utilisant Sodius MDWorkbench, un outil IDM conçu pour la création et manipulation des modèles et leur méta - modèles, ainsi que la définition et exécution des transformations des modèles associées / The main contribution of this thesis consists on the proposition and development a Model-driven Engineering (MDE) framework, in tandem with a component-based approach, for facilitating the design and implementation of Dynamic Partially Reconfigurable (DPR) Systems-on-Chip. The proposed methodology has been constructed around the Metadata-based Composition Framework paradigm, and based on common standards such as UML MARTE and the IEEE IP-XACT standard, an XML representation used for storing metadata about the IPs to be reused and of the platforms to be obtained at high-levels of abstraction. In fact, a componentizing process enables us to reuse the IP blocks, in UML MARTE, by wrapping them with PLB (static IPs) and proprietary (DPR blocks) interfaces. This is attained by reflecting the associated IP metadata to IP-XACT descriptions, and then to UML MARTE templates (IP reuse). Subsequently, these IP templates are used for composing a DPR model that can be exploited to create a Xilinx Platform Studio FPGA-design, through model transformations. The IP reflection and system generation chains were developed using Sodius MDWorkbench, an MDE tool conceived for the creation and manipulation of models and their meta-models, as well as the definition and execution of the associated transformation rules.

L’Ingénierie Dirigée par les Modèles (IDM) est une approche populaire pour le développement logiciel qui favorise l’utilisation de modèles au sein des processus de développement. Dans un processus de développement logiciel base sur l’IDM, le logiciel est développé en créant des modèles qui sont transformés successivement en d’autres modèles et éventuellement en code source. Quand l’IDM est utilisée pour le développement de logiciels complexes, la complexité des modèles et des transformations de modèles augmente, risquant d’affecter la fiabilité du processus de développement logiciel ainsi que le logiciel en résultant.Traditionnellement, la fiabilité des logiciels est assurée au moyen d’approches pour la vérification de logiciels, basées sur l’utilisation de techniques pour l’analyse formelle de systèmes et d’approches pour le test de logiciels. Pour assurer la fiabilité du processus IDM de développement logiciel, ces techniques ont en quelque sorte été adaptées pour essayer de s’assurer la correction des modèles et des transformations de modèles associées. L’objectif de cette thèse est de fournir de nouveaux mécanismes améliorant les approches existantes pour la vérification de modèles statiques, et d’analyser comment ces approches peuvent s’avérer utiles lors du test des transformations de modèles. / Model-Driven Engineering (MDE) is a popular approach to the development of software which promotes the use of models as first-Class citizens in the software development process. In a MDE-Based software development process, software is developed by creating models to be successively transformed into another models and eventually into the software source code. When MDE is applied to the development of complex software systems, the complexity of models and model transformations increase, thus risking both, the reliability of the software development process and the soundness of the resulting software. Traditionally, ensuring software correctness and absence of errors has been addressed by means of software verification approaches, based on the utilization of formal analysis techniques, and software testing approaches. In order to ensure the reliability of MDE-Based software development processes, these techniques have some how been adapted to try to ensure correctness of models and model transformations. The objective of this thesis is to provide new mechanisms to improve the landscape of approaches devoted to the verification of static models, and analyze how these static model verification approaches can be of assistance at the time of testing model transformations.

Actuellement, de nombreuses entreprises ont besoin de construire des versions\variantes légèrement différentes d'un même système. Ces versions partagent des points communs et des différences, le tout pouvant être géré à l'aide d'une approche ligne de produits (SPL). L'objectif principal d'une SPL est d'exploiter la personnalisation de masse, dans laquelle les produits sont réalisés pour répondre aux besoins spécifiques de chaque client. Pour répondre à ce besoin de personnalisation, les systèmes doivent être étendus de manière efficace, ou modifiés, configurés pour être utilisé dans un contexte particulier. Une approche encourageante consiste à connecter l'approche MDE (l'ingénierie dirigée par les modèles) à l'approche SPL – les SPL basées sur les modèles (MSPL). L'espace de conception, l'environnement du système logiciel que l'on construit (i.e., l'ingénierie du domaine) d'une MSPL est extrêmement complexe à gérer pour un ingénieur. Tout d'abord, le nombre possible des produits d'une MSPL est exponentielle au nombre d'éléments ou de décisions exprimé dans le modèle de variabilité. Ensuite, les modèles de produits dérivés doivent être conformes à de nombreuses règles liées au domaine métier mais aussi aux langages de modélisation utilisés. Troisièmement, le modèle de réalisation qui relie un modèle de variabilité et un modèle de base peut être très expressif. En plus, il faut ajouter que les ingénieurs système utilisent différents langages de modélisation dédiés dans le cadre de projets pour la réalisation de systèmes critiques. Nos contributions sont basées sur le fait qu'une solution générique, pour tous les domaines, et qui dérive des modèles corrects n'est pas réaliste, surtout si on prend en considération le contexte des systèmes complexes décrits précédemment. Nous proposons une approche indépendante du domaine pour générer des contre-exemples de MSPLs, révélant des erreurs de conceptions de modèles et supportant les parties prenantes à construire de meilleures MSPLs et des mécanismes de dérivation plus efficaces. Plus précisément, la première et principale contribution de la thèse est un processus systématique et automatisé, basé sur CVL (common variability language), pour la recherche aléatoire de contre-exemples de MSPL dans un langage donné. La seconde contribution de la thèse est un étude sur les mécanismes pour étendre la sémantique des moteurs de dérivation, offrant une approche basée sur des modèles à fin de personnaliser leurs sémantique opérationnelle. Dans la troisième contribution de la thèse, nous présentons une étude empirique à large échelle sur le langage Java en utilisant notre approche générative. La quatrième et dernière contribution de la thèse est une méthodologie pour intégrer notre travail dans une organisation qui cherche à mettre en œuvre les lignes de produit logiciels basées sur des modèles pour l'ingénierie des systèmes. / Systems Engineering is a complex and expensive activity in several kinds of companies, it imposes stakeholders to deal with massive pieces of software and their integration with several hardware components. To ease the development of such systems, engineers adopt a divide and conquer approach : each concern of the system is engineered separately, with several domain specific languages (DSL) and stakeholders. The current practice for making DSLs is to rely on the Model-driven Engineering (MDE. On the other hand, systems engineering companies also need to construct slightly different versions/variants of a same system; these variants share commonalities and variabilities that can be managed using a Software Product Line (SPL) approach. A promising approach is to ally MDE with SPL – Model-based SPLs (MSPL) – in a way that the products of the SPL are expressed as models conforming to a metamodel and well-formedness rules. The Common Variability Language (CVL) has recently emerged as an effort to standardize and promote MSPLs. Engineering an MSPL is extremely complex to an engineer: the number of possible products is exponential; the derived product models have to conform to numerous well- formedness and business rules; and the realization model that connects a variability model and a set of design models can be very expressive specially in the case of CVL. Managing variability models and design models is a non-trivial activity. Connecting both parts and therefore managing all the models is a daunting and error-prone task. Added to these challenges, we have the multiple different modeling languages of systems engineering. Each time a new modeling language is used for developing an MSPL, the realization layer should be revised accordingly. The objective of this thesis is to assist the engineering of MSPLs in the systems engineering field, considering the need to support it as earlier as possible and without compromising the existing development process. To achieve this, we provide a systematic and automated process, based on CVL, to randomly search the space of MSPLs for a given language, generating counterexamples that can server as antipatterns. We then provide ways to specialize CVL’s realization layer (and derivation engine) based on the knowledge acquired from the counterexamples. We validate our approach with four modeling languages, being one acquired from industry; the approach generates counterexamples efficiently, and we could make initial progress to increase the safety of the MSPL mechanisms for those languages, by implementing antipattern detection rules. Besides, we also analyse big Java programs, assessing the adequacy of CVL to deal with complex languages; it is also a first step to assess qualitatively the counterexamples. Finally, we provide a methodology to define the processes and roles to leverage MSPL engineering in an organization.

La multiplication des environnements logiciels pour la Modélisation & Simulation DEVS pose un problème de collaboration à la communauté scientifique. En effet, l'utilisation d'outils disparates rend l'échange, la réutilisation et la comparaison de modèles très difficiles, empêchant les scientifiques de s'appuyer sur des travaux précédents pour construire leurs modèles. L'interopérabilité des outils n'est pas le seul problème soulevé par le besoin de modèles toujours plus complexes. Au fur et à mesure que les modèles grossissent, leur développement devient plus difficile, notamment en termes de détection des erreurs de conception. D'autre part, la simulation de ces modèles demande de plus en plus de ressources. Par conséquent, il est nécessaire de concevoir des techniques pour améliorer la performance des simulateurs et pour fournir des fonctionnalités de vérification de modèle afin d'assister les scientifiques dans la conception de leurs modèles. Dans cette thèse, nous proposons deux approches innovantes pour la M&S DEVS qui s'attaquent aux problèmes susmentionnés. La première contribution décrite dans ce document est un environnement basé sur les modèles pour modéliser des systèmes avec le formalisme DEVS, intitulé SimStudio. Cet environnement repose sur l'Ingénierie Dirigée par les Modèles pour fournir un cadriciel de haut niveau dans lequel les scientifiques peuvent créer, éditer et visualiser des modèles, et générer automatiquement un ensemble d’artefacts, notamment des spécifications de modèles compatibles avec différents simulateurs DEVS. Le noyau de SimStudio est un métamodèle de DEVS, indépendant de toute plateforme, qui fournit un format pivot pour la représentation des modèles DEVS. En se basant sur ce métamodèle, nous avons développé plusieurs fonctionnalités de vérification de modèle ainsi que plusieurs transformations de modèle pouvant être utilisées pour générer automatiquement de la documentation, des diagrammes ou du code ciblant diverses plateformes DEVS. Ainsi, SimStudio fournit une preuve de concept des capacités d’intégration qu’un standard DEVS pourrait fournir ; en fait, le métamodèle présenté dans cette thèse pourrait potentiellement servir de base de réflexion pour un tel standard. La seconde contribution de cette thèse est DEVS-MetaSimulateur (DEVS-MS), une bibliothèque DEVS qui utilise la métaprogrammation pour générer des exécutables de simulation spécialisés et optimisés pour le modèle qu’ils traitent. Pour ce faire, la bibliothèque effectue un grand nombre d’opérations durant la compilation, résultant en un code de simulation où une grande partie de l’overhead de simulation a été éliminé. Les tests que nous avons effectués ont montré que les programmes générés étaient très efficaces, mais le gain de performance n’est pas la seule caractéristique intéressante de DEVS-MS. En effet, grâce à la métaprogrammation, DEVS-MS peut également partiellement vérifier à la compilation que les modèles sont corrects, c’est-à-dire que leurs caractéristiques sont bien conformes au formalisme DEVS. Les erreurs de modélisation sont ainsi détectées et signalées très tôt dans le cycle de développement, et avec un taux de détection bien meilleur que ne le permettrait des tests classiques. / The multiplication of software environments supporting DEVS Modeling & Simulation is becoming a hindrance to scientific collaboration. Indeed, the use of disparate tools in the community makes the exchange, reuse and comparison of models very difficult, preventing practitioners from building on previous works to devise models of ever-increasing complexity. Tool interoperability is not the only issue raised by the need for models of higher and higher complexity. As models grow, their development becomes more error-prone, and their simulation becomes more resource-consuming. Consequently, it is necessary to devise techniques for improving simulators performance and for providing thorough model verification to assist the practitioner during model design. In this thesis, we propose two innovative approaches for DEVS Modeling & Simulation that tackle the aforementioned issues. The first contribution described in this document is a model-driven environment for modeling systems with the DEVS formalism, named SimStudio. This environment relies on Model-Driven Engineering to provide a high-level framework where practitioners can create, edit and visualize models, and automatically generate multiple artifacts, most notably model specifications compatible with various DEVS simulators. The core of SimStudio is a platform-independent metamodel of the DEVS formalism, which provides a pivot format for DEVS models. Based on this metamodel, we developed several model verification features as well as many model transformations that can be used to automatically generate documentation, diagrams or code targeting various DEVS platforms. Thus, SimStudio gives a proof of concept of the integration capabilities that a DEVS standard would provide; as a matter of fact, the metamodel presented in this thesis could possibly serve as a basis for such a standard. The second contribution of this thesis is DEVS-MetaSimulator (DEVS-MS), a DEVS library relying on metaprogramming to generate simulation executables that are specialized and optimized for the model they handle. To do so, the library performs many computations during compilation, resulting in a simulation code where most overhead have been eliminated. The tests we conducted showed that the generated programs were very efficient, but the performance gain is not the only feature of DEVS-MS. Indeed, through metaprogramming, DEVS-MS can also assert the correctness of models by verifying model characteristics at compile-time, detecting and reporting modeling errors very early in the development cycle and with better confidence than what could be achieved with classical testing.

No description available.

Le cycle de vie d'un réseau de capteurs implique plusieurs étapes, telles que le dimensionnement du réseau, le développement de logiciels embarqués, la réalisation de matériels, des analyses et des simulations, le déploiement physique, l'exploitation des données et la maintenance du réseau. Tout au long de ce cycle, plusieurs outils spécifiques sont utilisés. Il est donc nécessaire de décrire manuellement les caractéristiques du réseau de capteurs dans chacun de ces outils en utilisant leurs propres langages. Il en résulte des coûts de développement importants et éventuellement des incohérences entre les différentes descriptions. Pour répondre à cette problématique, nous proposons une méthodologie basée sur l'approche MDE (Model Driven Engineering). Elle vise à couvrir toutes les étapes du cycle de vie d'un réseau de capteurs. Tous les concepts et les caractéristiques d'un réseau de capteurs sont décrits à l'aide d'un métamodèle. A partir de ce référentiel, il est possible d'extraire, à chaque étape du cycle de vie, une ou plusieurs facettes. Chaque facette est présentée et éditée avec l'outil le plus adéquat en créant des passerelles vers des outils tiers. Afin de mettre en œuvre la méthodologie proposée, un Framework est développé pour offrir un environnement de description multi-facettes : architecture réseau, architecture matérielle, architecture logicielle, flux de données et environnement physique. Un exemple de passerelle entre le Framework et un simulateur existant (Omnet++) a été développé pour estimer les performances des réseaux de capteurs. Le Framework permet la génération automatique des scripts de simulation ainsi que des codes sources pour les nœuds du réseau / The life cycle of a sensor network involves several steps, including network sizing, embedded software development, hardware design, analysis and simulation, physical deployment, data exploitation, and network maintenance. Throughout this cycle, several specific tools are used. It is therefore necessary to manually describe the characteristics of the sensor network in each of these tools using their own languages. This results in significant development costs and potential inconsistencies between the different descriptions. To address this problem, we propose a methodology based on model driven engineering approach. It aims to cover all life cycle steps of a sensor network. All concepts and characteristics of a sensor network are described using a metamodel. From this referential, it is possible to extract, at each step of the life cycle, one or more facets. Each facet is presented and edited with the most appropriate tool by creating gateways to external tools.In order to implement the proposed methodology, a Framework is developed to provide a multi-facets environment: network architecture, hardware architecture, software architecture, data flow and physical environment. An example of a gateway between the Framework and an existing simulator (Omnet++) has been developed to estimate sensor network performances. The Framework allows automatic generation of simulation scripts as well as source codes for network nodes

Alors que les systèmes embarqués sont de plus en plus nombreux, complexes, connectés et chargés de tâches critiques, la question de comment intégrer l'analyse précise de sécurité à la conception de systèmes embarqués doit trouver une réponse. Dans cette thèse, nous étudions comment les méthodes de vérification formelle automatiques peuvent aider les concepteurs de systèmes embarqués à évaluer l'impact des modifications logicielles et matérielles sur la sécurité des systèmes. Une des spécificités des systèmes embarqués est qu'ils sont décrits sous la forme de composants logiciels et matériels interagissant. Vérifier formellement de tels systèmes demande de prendre tous ces composants en compte. Nous proposons un exemple d'un tel système (basé sur Intel SGX) qui permet d'établir un canal sécurisé entre un périphérique et une application. Il est possible d'en vérifier un modèle de haut-niveau ou une implémentation bas-niveau. Ces deux niveaux diffèrent dans le degré d'intrication entre matériel et logiciel. Dans le premier cas, nous proposons une approche orientée modèle, à la fois au niveau partitionnement et conception logicielle, permettant une description à haut niveau d'abstraction du matériel et du logiciel et permettant une transformation de ces modèles en une spécification formelle sur laquelle une analyse de sécurité peut être effectuée avec l'outil ProVerif. Dans le second cas, nous considérons une implémentation logicielle et un modèle matériel plus concret pour effectuer des analyses de sécurité plus précises toujours avec ProVerif. / As embedded systems become more complex, more connected and more involved in critical tasks, the question of how strict security analysis can be performed during embedded system design needs to be thoroughly addressed. In this thesis, we study how automated formal verification can help embedded system designers in evaluating the impact of hardware and software modifications on the security of the whole system. One of the specificities of embedded system design-which is of particular interest for formal verification-is that the system under design is described as interacting hardware and software components. Formally verifying these systems requires taking both types of components into account. To illustrate this fact, we propose an example of a hardware/software co-design (based on Intel SGX) that provides a secure channel between a peripheral and an application. Formal verification can be performed on this system at different levels: from a high-level view (without describing the implementations) or from a low-level implementation. These two cases differ in terms of how tightly coupled the hardware and software components are. In the first case, we propose a model-based approach-for both the partitioning and software design phases- which enables us to describe software and hardware with high-level models and enables a transformation of these models into a formal specification which can be formally analyzed by the ProVerif tool. In the second case, we consider a software implementation and a more concrete

The industrial manufacturing of today is achieved through the use of programmable logic controllers (PLC). The way PLCs are programmed remains largely unchanged since their conception 40 years ago, but complexity and software size have increased, and requirements have becomemore elaborate. Model-driven engineering (MDE) practices, formal verification and automated testing could help manage these challenges. This study seeks to improve development practices in the context of a company that delivers automation projects. Through design science methodology the state of the field is investigated and an artefact is developed. The artefact shows potential benefits resulting from the introduction of model-driven code generation, which is evaluated through an experiment with engineers. Our results indicate the engineers may benefit from incorporating generated code in their work.

El objetivo principal de esta tesis es el desarrollo de un sistema de análisis de la marcha basado en visión que permita clasificar la marcha patológica. Este objetivo general se divide en tres subobjetivos específicos más concretos: definición formal de la marcha, especificación e implementación de un sistema de obtención de parámetros de la marcha basado en visión y clasificación de la marcha patológica. En el primer subobjetivo, definición formal de la marcha, nuestros esfuerzos consisten en obtener una definición de la marcha que incluya la visión por computador pero sin excluir otros métodos y que sea lo suficientemente abierta como para incluir todos los casos de marcha humana. La definición propuesta es la siguiente: "Gait is the anthropomorphic upright self-displacement, in an alternating stepping of two feet, with no additional fulcra, keeping at least a point of support at every time, on a horizontal or slightly inclined surface." A partir de esta definición, las variables que consideramos son tiempos y longitudes de paso y zancada, tiempos de apoyo monopodal y bipodal, velocidad, cadencia, etc... Para el segundo subobjetivo, especificación e implementación de un sistema de obtención de parámetros de la marcha basado en visión, nos centramos en el análisis de la marcha mediante visión por computador utilizando únicamente una cámara RGB, que obtenga imágenes laterales y frontales del sujeto. El algoritmo propuesto es capaz de extraer las variables de la marcha, establecidas en la definición del objetivo de especificación, con suficiente precisión, de modo que la marcha puede ser interpretada y clasificada. La decisión de limitar la infraestructura necesaria a una única cámara RGB, obedece al interés por abaratar los costes del sistema y que sea sostenible medioambientalmente, ya que no requiere de energía adicional para capturar la imagen, sino que utiliza la radiación lumínica que inunda el escenario, ya sea de forma natural o artificial. Este sistema actúa como interfaz de entrada del subobjetivo tres que son las variables de la marcha propuestas en el subobjetivo uno. Por tanto, el subobjetivo dos puede ser reemplazado por otro sistema basado en otro fenómeno como es el caso de un sistema inercial, siempre y cuando pueda proporcionar las variables definidas en el subobjetivo uno. El subobjetivo tres, clasificador de la marcha patológica, usa las variables proporcionadas por el sistema del subobjetivo dos para caracterizar la marcha y clasificarla. Mediante una serie de casos de entrenamiento, el sistema genera los modelos de marcha patológica y normal. A partir de estos modelos, el clasificador es capaz de determinar a qué modelo pertenece la entrada de parámetros de la marcha proporcionada por el subobjetivo dos. El objetivo de formalización nos ha llevado a profundizar en los aspectos conceptuales y procedimentales del conocimiento y de su creación, con la consecuencia de aportar sendas definiciones para problema y modelo, así como hallar una justificación formal, basada en la teoría de conjuntos, que confiere coherencia causal al método experimental. Además de encontrar formalmente la justificación causal del método científico, hemos podido encajar en ese marco formal los enfoques divide et vinces, model driven y top-down de resolución de problemas ingenieriles. Al tiempo que hemos encontrado que la técnica top-down de diseño es coincidente con el método científico de resolución de problemas, el método bottom-up es coherente con la implementación de prototipos, lo cual justifica la restricción de su utilización al diseño de instancias para las que ya se conoce solución.

Nous proposons dans cette thèse une nouvelle approche pour l'exploration d’espaces de conception. Plus précisément, nous utilisons la composition de transformations de modèles pour automatiser la production d'alternatives architecturales, et les algorithmes génétiques pour explorer et identifier des alternatives architecturales quasi-optimales. Les transformations de modèles sont des solutions réutilisables et peuvent être intégrées dans des algorithmes génétiques et ainsi être combinées avec des opérateurs génétiques tels que la mutation et le croisement. Grâce à cela, nous pouvons utiliser (ou réutiliser) différentes transformations de modèles implémentant différents patrons de conception sans pour autant modifier l’environnement d’optimisation. En plus de cela, les transformations de modèles peuvent être validées (par rapport aux contraintes structurelles) en amont et ainsi rejeter avant l’exploration les transformations générant des alternatives architecturales incorrectes. Enfin, les transformations de modèles peuvent être chainées entre elles afin de faciliter leur maintenance, leur réutilisabilité et ainsi concevoir des modèles plus détaillés et plus complexes se rapprochant des systèmes industrielles. A noter que l’exploration de chaines de transformations de modèles a été intégrée dans l’environnement d’optimisation. / In this thesis, we propose a new exploration approach to tackle design space exploration problems involving multiple conflicting non functional properties. More precisely, we propose the use of model transformation compositions to automate the production of architectural alternatives, and multiple-objective evolutionary algorithms to identify near-optimal architectural alternatives. Model transformations alternatives are mapped into evolutionary algorithms and combined with genetic operators such as mutation and crossover. Taking advantage of this contribution, we can (re)-use different model transformations, and thus solve different multiple-objective optimization problems. In addition to that, model transformations can be chained together in order to ease their maintainability and re-usability, and thus conceive more detailed and complex systems.