• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 1
  • 1
  • Tagged with
  • 2
  • 2
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
1

Constructing Semantically Sound Object-Logics for UML/OCL Based Domain-Specific Languages / Construction de Logiques-Objet Sémantiquement Correct pour des Langages à Domaines Spécifiques Basés sur UML/OCL

Tuong, Frédéric 06 April 2016 (has links)
Les langages de spécifications basés et orientés objets (comme UML/OCL, JML, Spec#, ou Eiffel) permettent la création et destruction, la conversion et tests de types dynamiques d'objets statiquement typés. Par dessus, les invariants de classes et les opérations de contrat peuvent y être exprimés; ces derniers représentent les éléments clés des spécifications orientées objets. Une sémantique formelle des structures de données orientées objets est complexe : des descriptions imprécises mènent souvent à différentes interprétations dans les outils qui en résultent. Dans cette thèse, nous démontrons comment dériver un environnement de preuves moderne comme un méta-outil pour la définition et l'analyse de sémantique formelle de langages de spécifications orientés objets. Étant donné une représentation d'un langage particulier plongé en Isabelle/HOL, nous construisons pour ce langage un environnement étendu d'Isabelle, à travers une méthode de génération de code particulière, qui implique notamment plusieurs variantes de génération de code. Le résultat supporte l'édition asynchrone, la vérification de types, et les activités de déduction formelle, tous "hérités" d'Isabelle. En application de cette méthode, nous obtenons un outil de modélisation orienté objet pour du UML/OCL textuel. Nous intégrons également des idiomes non nécessairement présent dans UML/OCL --- en d'autres termes, nous développons un support pour des dialectes d'UML/OCL à domaine spécifique. En tant que construction méta, nous définissons un méta-modèle d'une partie d'UML/OCL en HOL, un méta-modèle d'une partie de l'API d'Isabelle en HOL, et une fonction de traduction entre eux en HOL. Le méta-outil va alors exploiter deux procédés de générations de code pour produire soit du code raisonnablement efficace, soit du code raisonnablement lisible. Cela fournit donc deux modes d'animations pour inspecter plus en détail la sémantique d'un langage venant d'être plongé : en chargeant à vitesse réelle sa sémantique, ou simplement en retardant à un autre niveau "méta" l'expérimentation précédente pour un futur instant de typage en Isabelle, que ce soit pour des raisons de performances, de tests ou de prototypages. Remarquons que la génération de "code raisonnablement efficace", et de "code raisonnablement lisible" incluent la génération de code tactiques qui prouvent une collection de théorèmes formant une théorie de types de données orientés objets d'un modèle dénotationnel : étant donné un modèle de classe UML/OCL, les preuves des propriétés pertinentes aux conversions, tests de types, constructeurs et sélecteurs sont traitées automatiquement. Cette fonctionnalité est similaire aux paquets de théories de types de données présents au sein d'autres prouveurs de la famille HOL, à l'exception que certaines motivations ont conduit ce travail présent à programmer des tactiques haut-niveaux en HOL lui-même. Ce travail prend en compte les plus récentes avancées du standard d'UML/OCL 2.5. Par conséquent, tous les types UML/OCL ainsi que les types logiques distinguent deux éléments d'exception différents : invalid (exception) et null (élément non-existant). Cela entraîne des conséquences sur les propriétés aussi bien logiques qu'algébriques des structures orientées objets résultant des modèles de classes. Étant donné que notre construction est réduite à une séquence d'extension conservative de théorie, notre approche peut garantir la correction logique du langage entier considéré, et fournit une méthodologie pour étendre formellement des langages à domaine spécifique. / Object-based and object-oriented specification languages (likeUML/OCL, JML, Spec#, or Eiffel) allow for the creation and destruction, casting and test for dynamic types of statically typed objects. On this basis, class invariants and operation contracts can be expressed; the latter represent the key elements of object-oriented specifications. A formal semantics of object-oriented data structures is complex: imprecise descriptions can often imply different interpretations in resulting tools. In this thesis we demonstrate how to turn a modern proof environment into a meta-tool for definition and analysis of formal semantics of object-oriented specification languages. Given a representation of a particular language embedded in Isabelle/HOL, we build for this language an extended Isabelle environment by using a particular method of code generation, which actually involves several variants of code generation. The result supports the asynchronous editing, type-checking, and formal deduction activities, all "inherited" from Isabelle. Following this method, we obtain an object-oriented modelling tool for textual UML/OCL. We also integrate certain idioms not necessarily present in UML/OCL --- in other words, we develop support for domain-specific dialects of UML/OCL. As a meta construction, we define a meta-model of a part of UML/OCL in HOL, a meta-model of a part of the Isabelle API in HOL, and a translation function between both in HOL. The meta-tool will then exploit two kinds of code generation to produce either fairly efficient code, or fairly readable code. Thus, this provides two animation modes to inspect in more detail the semantics of a language being embedded: by loading at a native speed its semantics, or just delay at another "meta"-level the previous experimentation for another type-checking time in Isabelle, be it for performance, testing or prototyping reasons. Note that generating "fairly efficient code", and "fairly readable code" include the generation of tactic code that proves a collection of theorems forming an object-oriented datatype theory from a denotational model: given a UML/OCL class model, the proof of the relevant properties for casts, type-tests, constructors and selectors are automatically processed. This functionality is similar to the datatype theory packages in other provers of the HOL family, except that some motivations have conducted the present work to program high-level tactics in HOL itself. This work takes into account the most recent developments of the UML/OCL 2.5 standard. Therefore, all UML/OCL types including the logic types distinguish two different exception elements: invalid (exception) and null (non-existing element). This has far-reaching consequences on both the logical and algebraic properties of object-oriented data structures resulting from class models. Since our construction is reduced to a sequence of conservative theory extensions, the approach can guarantee logical soundness for the entire considered language, and provides a methodology to soundly extend domain-specific languages.
2

Lightning induced voltages in cables of power production centers / Tensions Induites par une agression foudre dans les câbles de contrôle-mesure des centres de production d'énergie

Diaz Pulgar, Luis Gerardo 29 November 2016 (has links)
Lorsqu’un bâtiment d’un centre de production d’électricité est frappé par la foudre, il se produit une dangereuse circulation de courants dans tous les composants connectés au bâtiment: les murs, le réseau de terre, et les câbles sortant du bâtiment. L’intérêt du présent travail est d’étudier les tensions transitoires aux extrémités de ces câbles, en particulier des câbles contrôle mesure, dans la mesure où ces câbles sont connectés à des équipements électroniques susceptibles d’être endommagés par des perturbations électromagnétiques engendrées par la foudre. Une approche basée sur la résolution numérique des équations de Maxwell via une méthode FDTD est adoptée. Notamment le formalisme de Holland et Simpson est utilisé pour modéliser toutes les structures constituées d’un réseau de fils minces: l’armature métallique du bâtiment, la grille en cuivre du réseau de terre, la galerie de béton et le câble coaxial de contrôle mesure. Une validation des modèles électromagnétiques développés pour chaque composant du site industriel est présentée. Une analyse de sensibilité est conduite pour déterminer l’influence des paramètres du système. En outre, la technique des plans d’expérience est utilisée pour générer un méta-modèle qui prédit la tension maximale induite aux extrémités du câble en fonction des paramètres les plus influents. Cela représentent un outil de calcul précis et informatiquement efficace pour évaluer la performance foudre des câbles de contrôle et de mesure. / When lightning strikes a building in a Power Generation Center, dangerous currents propagates through all the components connected to the building structure: The walls, the grounding grid, and the cables leaving the building. It is the interest of this work to study the transient voltages at the terminations of these cables external to the building.Particularly, the Instrumentation and Measure (IM) cables, since they are connected to electronic equipment susceptible of damage or malfunctioning due to lightning ElectroMagnetic perturbations. A full wave approach based on the numerical solution of Maxwell’s equations through the FDTD algorithm is adopted. Notably, the formalism of Holland and Simpson is used to model all the structures composed of thin wires: the building steel structure, the grounding copper grid, the concrete cable ducts and the coaxial IM cables. A validation of the model developed for each component is presented. A sensitivity analysis is performed in order to the determine the main parameters that configure the problem. Also, the Design of Experiments (DoE) technique is used to generate a meta-model that predicts the peak induced voltages in the cable terminations, as a function of the main parameters that configure the industrial site. This represents an accurate, and computationally efficient tool to assess lightning performance of IM cables.

Page generated in 0.0549 seconds