Tesi: "Interopérabilité des systèmes de preuve"

1

Cauderlier, Raphaël. "Object-Oriented Mechanisms for Interoperability Between Proof Systems". Thesis, Paris, CNAM, 2016. http://www.theses.fr/2016CNAM1065/document.

Testo completo

Abstract (sommario):

Dedukti est un cadre logique résultant de la combinaison du typage dépendant et de la réécriture. Il permet d'encoder de nombreux systèmes logiques au moyen de plongements superficiels qui préservent la notion de réduction. Ces traductions de systèmes logiques dans un format commun sont une première étape nécessaire à l'échange de preuves entre ces systèmes. Cet objectif d'interopérabilité des systèmes de preuve est la motivation principale de cette thèse. Pour y parvenir, nous nous inspirons du monde des langages de programmation et plus particulièrement des langages orientés-objet parce qu'ils mettent en œuvre des mécanismes avancés d'encapsulation, de modularité et de définitions par défaut. Pour cette raison, nous commençons par une traduction superficielle d'un calcul orienté-objet en Dedukti. L'aspect le plus intéressant de cette traduction est le traitement du sous-typage. Malheureusement, ce calcul orienté-objet ne semble pas adapté à l'incorporation de traits logiques. Afin de continuer, nous devons restreindre les mécanismes orientés-objet à des mécanismes statiques, plus faciles à combiner avec la logique et apparemment suffisant pour notre objectif d'interopérabilité. Une telle combinaison de mécanismes orientés-objet et de logique est présente dans l'environnement FoCaLiZe donc nous proposons un encodage superficiel de FoCaLiZe dans Dedukti. Les difficultés principales proviennent de l'intégration de Zenon, le prouveur automatique de théorèmes sur lequel FoCaLiZe repose, et de la traduction du langage d'implantation fonctionnel de FoCaLiZe qui présente deux constructions qui n'ont pas de correspondance simple en Dedukti : le filtrage de motif local et la récursivité. Nous démontrons finalement comment notre encodage de FoCaLiZe dans Dedukti peut servir en pratique à l'interopérabilité entre des systèmes de preuve à l'aide de FoCaLiZe, Zenon et Dedukti. Pour éviter de trop renforcer la théorie dans laquelle la preuve finale est obtenue, nous proposons d'utiliser Dedukti en tant que méta-langage pour éliminer des axiomes superflus
Dedukti is a Logical Framework resulting from the combination ofdependent typing and rewriting. It can be used to encode many logical systems using shallow embeddings preserving their notion of reduction. These translations of logical systems in a common format are a necessary first step for exchanging proofs between systems. This objective of interoperability of proof systems is the main motivation of this thesis.To achieve it, we take inspiration from the world of programming languages and more specifically from object-oriented languages because they feature advanced mechanisms for encapsulation, modularity, and default definitions. For this reason we start by a shallow translation of an object calculus to Dedukti. The most interesting point in this translation is the treatment of subtyping. Unfortunately, it seems very hard to incorporate logic in this object calculus. To proceed, object-oriented mechanisms should be restricted to static ones which seem enough for interoperability. Such a combination of static object-oriented mechanisms and logic is already present in the FoCaLiZe environment so we propose a shallow embedding of FoCaLiZe in Dedukti. The main difficulties arise from the integration of FoCaLiZe automatic theorem prover Zenon and from the translation of FoCaLiZe functional implementation language featuring two constructs which have no simple counterparts in Dedukti: local pattern matching and recursion. We then demonstrate how this embedding of FoCaLiZe to Dedukti can be used in practice for achieving interoperability of proof systems through FoCaLiZe, Zenon, and Dedukti. In order to avoid strengthening to much the theory in which the final proof is expressed, we use Dedukti as a meta-language for eliminating unnecessary axioms

Gli stili APA, Harvard, Vancouver, ISO e altri

2

Cauderlier, Raphaël. "Object-Oriented Mechanisms for Interoperability Between Proof Systems". Electronic Thesis or Diss., Paris, CNAM, 2016. http://www.theses.fr/2016CNAM1065.

Testo completo

Abstract (sommario):

Dedukti est un cadre logique résultant de la combinaison du typage dépendant et de la réécriture. Il permet d'encoder de nombreux systèmes logiques au moyen de plongements superficiels qui préservent la notion de réduction. Ces traductions de systèmes logiques dans un format commun sont une première étape nécessaire à l'échange de preuves entre ces systèmes. Cet objectif d'interopérabilité des systèmes de preuve est la motivation principale de cette thèse. Pour y parvenir, nous nous inspirons du monde des langages de programmation et plus particulièrement des langages orientés-objet parce qu'ils mettent en œuvre des mécanismes avancés d'encapsulation, de modularité et de définitions par défaut. Pour cette raison, nous commençons par une traduction superficielle d'un calcul orienté-objet en Dedukti. L'aspect le plus intéressant de cette traduction est le traitement du sous-typage. Malheureusement, ce calcul orienté-objet ne semble pas adapté à l'incorporation de traits logiques. Afin de continuer, nous devons restreindre les mécanismes orientés-objet à des mécanismes statiques, plus faciles à combiner avec la logique et apparemment suffisant pour notre objectif d'interopérabilité. Une telle combinaison de mécanismes orientés-objet et de logique est présente dans l'environnement FoCaLiZe donc nous proposons un encodage superficiel de FoCaLiZe dans Dedukti. Les difficultés principales proviennent de l'intégration de Zenon, le prouveur automatique de théorèmes sur lequel FoCaLiZe repose, et de la traduction du langage d'implantation fonctionnel de FoCaLiZe qui présente deux constructions qui n'ont pas de correspondance simple en Dedukti : le filtrage de motif local et la récursivité. Nous démontrons finalement comment notre encodage de FoCaLiZe dans Dedukti peut servir en pratique à l'interopérabilité entre des systèmes de preuve à l'aide de FoCaLiZe, Zenon et Dedukti. Pour éviter de trop renforcer la théorie dans laquelle la preuve finale est obtenue, nous proposons d'utiliser Dedukti en tant que méta-langage pour éliminer des axiomes superflus
Dedukti is a Logical Framework resulting from the combination ofdependent typing and rewriting. It can be used to encode many logical systems using shallow embeddings preserving their notion of reduction. These translations of logical systems in a common format are a necessary first step for exchanging proofs between systems. This objective of interoperability of proof systems is the main motivation of this thesis.To achieve it, we take inspiration from the world of programming languages and more specifically from object-oriented languages because they feature advanced mechanisms for encapsulation, modularity, and default definitions. For this reason we start by a shallow translation of an object calculus to Dedukti. The most interesting point in this translation is the treatment of subtyping. Unfortunately, it seems very hard to incorporate logic in this object calculus. To proceed, object-oriented mechanisms should be restricted to static ones which seem enough for interoperability. Such a combination of static object-oriented mechanisms and logic is already present in the FoCaLiZe environment so we propose a shallow embedding of FoCaLiZe in Dedukti. The main difficulties arise from the integration of FoCaLiZe automatic theorem prover Zenon and from the translation of FoCaLiZe functional implementation language featuring two constructs which have no simple counterparts in Dedukti: local pattern matching and recursion. We then demonstrate how this embedding of FoCaLiZe to Dedukti can be used in practice for achieving interoperability of proof systems through FoCaLiZe, Zenon, and Dedukti. In order to avoid strengthening to much the theory in which the final proof is expressed, we use Dedukti as a meta-language for eliminating unnecessary axioms

Gli stili APA, Harvard, Vancouver, ISO e altri

3

Hondet, Gabriel. "Expressing predicate subtyping in computational logical frameworks". Electronic Thesis or Diss., université Paris-Saclay, 2022. http://www.theses.fr/2022UPASG070.

Testo completo

Abstract (sommario):

Le typage permet d'apporter de la sûreté dans la programmation, et il est utilisé au coeur de la majorité des systèmes de preuve. Plus un système de types est expressif, plus il est aisé d'y encoder des invariantsqui seront vérifiés mécaniquement lors du typage. Les types dépendants sont une extension des types simples dans laquelle les types peuvent dépendre de valeurs. Ils permettent par exemple de définir les vecteurs paramétrés par leur longueur. Le sous-typage par prédicat est une autre extension des types simples, dans laquelle les types peuvent être définis par des prédicats. Un sous-type défini par un prédicat, généralement noté { x : A | P(x) }, est habité par les éléments t de type A pour lesquels P(t) est vrai. Cette extension fournit un système de type très riche et intuitif, mais qui rend le typage indécidable.Cet ouvrage est dédié à l'encodage du sous-typage par prédicats dans Dedukti, un cadre logique avec des règles de calcul. On commence par encoder une version explicite du sous-typage par prédicats pour lequel un habitant de { x: A | P(x) } est syntaxiquement différent d'un habitant de A. On montre que tout jugement dérivable dans cette version du sous-typage par prédicat peut être encodé en un jugement dérivable du cadre logique.Le sous-typage par prédicat est souvent utilisé de manière implicite, sans différence syntaxique entre les habitants de A et les habitants de { x: A | P(x) }. On enrichit le cadre logique avec un système de raffinement des termes qui pourra ajouter ces marqueurs syntaxiques. Ce raffineur peut traduire des jugements typables avec du sous-typage par prédicat implicite en des jugements typable avec du sous-typage explicite.L'assistant à la preuve pvs utilise abondamment le sous-typage par prédicat. On montre comment sa bibliothèque standard peut être exportée vers Dedukti. Par ailleurs, PVS ne préserve que des traces de preuves. Dans la pénultième section, on décrit une procédure pour générer des preuves complètes à partir des traces laissées par PVS.La dernière section détaille une architecture pour l'entrepôt et l'échange de preuves formelles, afin de promouvoir l'interopérabilité
Safe programming as well as most proof systems rely on typing. The more a type system is expressive, the more these types can be used to encode invariants which are therefore verified mechanically through type checking procedures. Dependent types extend simple types by allowing types to depend on values. For instance, it allows to define the types of lists of a certain length. Predicate subtyping is another extension of simple type theory in which types can be defined by predicates. A predicate subtype, usually noted {x: A | P(x)}, is inhabited by elements t of type A for which P(t) is true. This extension provides an extremely rich and intuitive type system, which is at the heart of the proof assistant PVS, at the cost of making type checking undecidable.This work is dedicated to the encoding of predicate subtyping in Dedukti: a logical framework with computation rules. We begin with the encoding of explicit predicate subtyping for which the terms in {x: A | P(x)} and terms of Aare syntactically different. We show that any derivable judgement of predicate subtyping can be encoded into a derivable judgement of the logical framework. Predicate subtyping, is often used implicitly: with no syntactic difference between terms of type A and terms of type {x: A | P(x) }. We enrich our logical framework with a term refiner which can add these syntactic markers. This refiner can be used to refine judgements typed with implicit predicate subtyping into explicited judgements.The proof assistant PVS uses extensively predicate subtyping. We show how its standard library can be exported to Dedukti. Because PVS only store proof traces rather than complete proof terms, we sketch in the penultimate section a procedure to generate complete proof terms from these proof traces.The last section provides the architecture of a repository dedicated to the exchange of formal proofs. The goal of such a repository is to categorise and store proofs encoded in Dedukti to promote interoperability

Gli stili APA, Harvard, Vancouver, ISO e altri

4

Felicissimo, Thiago. "Generic bidirectional typing in a logical framework for dependent type theories". Electronic Thesis or Diss., université Paris-Saclay, 2024. http://www.theses.fr/2024UPASG049.

Testo completo

Abstract (sommario):

Les théories des types dépendants sont des systèmes formels qui peuvent être utilisés à la fois comme langages de programmation et pour la formalisation des mathématiques, et constituent la base de plusieurs assistants de preuve tels que Coq et Agda. Afin d'unifier leur étude, les Logical Frameworks (LFs) fournissent un méta-langage unifié permettant de définir ces théories, dans lequel diverses notions universelles sont intégrées par défaut et où des méta-théorèmes génériques peuvent être prouvés. Cette thèse se concentre sur les LFs conçus pour être implémentés, avec pour objectif de fournir des type-checkers génériques. Notre principale contribution est un nouveau LF permettant de représenter les théories des types avec leurs syntaxes non annotées habituelles. La clé pour permettre de supprimer des annotations sans compromettre la décidabilité du typage est l'intégration du typage bidirectionnel, une discipline dans laquelle le jugement de typage est décomposé en modes d'inférence et de checking. Si le typage bidirectionnel est déjà bien étudié dans la littérature, l'une des contributions centrales de notre travail est sa formulation dans un LF, ce qui donne un traitement générique pour toutes les théories définissables dans notre système. Notre proposition a été implémentée dans le type-checker générique BiTTs, permettant son utilisation avec diverses théories.En plus de notre contribution principale, nous proposons des avancés dans l'étude de Dedukti, un LF appartenant à la même famille que le système que nous proposons. Tout d'abord, nous revisitons le problème de la correction des encodages dans Dedukti en proposant une méthodologie qui permet de démontrer plus facilement la conservativité. De plus, nous montrons comment Dedukti peut être utilisé en pratique comme outil de traduction de preuves, en proposant une transformation pour partager des preuves avec des systèmes prédicatifs. Cette transformation a permis la traduction de preuves de Matita vers Agda, aboutissant aux toutes premières preuves en Agda du Petit Théorème de Fermat et du Postulat de Bertrand
Dependent type theories are formal systems that can be used both as programming languages and for the formalization of mathematics, and constitute the foundation of popular proof assistants such as Coq and Agda. In order to unify their study, Logical Frameworks (LFs) provide a unified meta-language for defining such theories in which various universal notions are built in by default and metatheorems can be proven in a theory-independent way. This thesis focuses on LFs designed with implementation in mind, with the goal of providing generic type-checkers. Our main contribution is a new such LF which allows for representing type theories with their usual non-annotated syntaxes. The key to allowing the removal of annotations without jeopardizing decidability of typing is the integration of bidirectional typing, a discipline in which the typing judgment is decomposed into inference and checking modes. While bidirectional typing has been well known in the literature for quite some time, one of the central contributions of our work is that, by formulating it in an LF, we give it a generic treatment for all theories fitting our framework. Our proposal has been implemented in the generic type-checker BiTTs, allowing it to be used in practice with various theories. In addition to our main contribution, we also advance the study of Dedukti, a sibling LF of our proposed framework. First, we revisit the problem of showing that theories are correctly represented in Dedukti by proposing a methodology for encodings which allows for showing their conservativity easily. Furthermore, we demonstrate how Dedukti can be used in practice as a tool for translating proofs by proposing a transformation for sharing proofs with predicative systems. This transformation has allowed for the translation of proofs from Matita to Agda, yielding the first-ever Agda proofs of Fermat's Little Theorem and Bertrand's Postulate

Gli stili APA, Harvard, Vancouver, ISO e altri

5

Besançon, Léo. "Interopérabilité des Systèmes Blockchains". Thesis, Lyon, 2021. https://tel.archives-ouvertes.fr/tel-03789639.

Testo completo

Abstract (sommario):

La Blockchain est une technologie disruptive. Elle s'intègre dans un écosystème décentralisé d’applications aux propriétés intéressantes : la transparence des transactions, l’auditabilité des applications, ou encore la résistance à la censure. Les domaines d'application sont variés, de la finance à la santé ou au jeu vidéo. La technologie a évolué depuis sa création en 2008 et possède de nombreuses perspectives. Néanmoins, le domaine rencontre de nombreux défis. Chaque Blockchain utilisant ses propres standards et modèles économiques, il subit notamment un manque d’interopérabilité à différents niveaux : entre les différents projets d'une Blockchain, entre les différentes Blockchains, ainsi qu’entre les Blockchains et les autres systèmes. Un aspect important de l'interopérabilité des systèmes Blockchains est leur interopérabilité sémantique, qui nécessite de définir formellement les concepts liés. Un autre défi est la conception d'applications Blockchains décentralisées. Ces applications intègrent la technologie Blockchain, mais aussi d'autres services qui permettent de satisfaire les contraintes de l'application pour lesquelles la Blockchain n'est pas adaptée. Cependant, il est complexe de choisir les services Blockchain les plus adaptés à une application donnée. Cette thèse a pour objectif la proposition d’un cadre permettant d’améliorer l’interopérabilité des applications Blockchain décentralisées. Pour cela, nous développons une méthodologie d'aide à la conception de ces applications, ainsi qu'une ontologie Blockchain qui aide à formaliser leurs concepts. Ce cadre est validé dans le domaine des jeux vidéo Blockchain. Cet environnement est complexe, car il nécessite le partage de données volumineuses. De plus, les contraintes de latence doivent être respectées
Blockchains are a disruptive technology. They enable an ecosystem for decentralized applications with interesting properties: transaction transparency, application auditability or censorship resistance. It has applications in various fields, such as finance, healthcare or video games. It has evolved a lot since its creation in 2008, and presents numerous perspectives. However, the field faces many challenges, in particular a lack of interoperability at several levels: between projects on a same Blockchain, between different Blockchains, or between Blockchains and other systems. One important aspect of Blockchain systems interoperability is semantic interoperability. It relies on formal definitions of the related concepts. Another challenge is the design of decentralized Blockchain applications. These applications integrate Blockchain technology, but also other services that satisfy the constraints of the application that Blockchain is not suitable for. However, it is complex to choose the most suited Blockchain service for a given application. With this PhD work, we propose a framework that can improve interoperability for decentralized Blockchain applications. We achieve this with the design of a methodology and a Blockchain ontology that help formalize the concepts related to an application. This framework is validated in the context of Blockchain video game development. It is a complex use case, as it needs to share storage intensive data and satisfy the latency constraints

Gli stili APA, Harvard, Vancouver, ISO e altri

6

Kirchner, Florent. "Systèmes de preuve interopérables". Phd thesis, Ecole Polytechnique X, 2007. http://pastel.archives-ouvertes.fr/pastel-00003192.

Testo completo

Abstract (sommario):

Les developpements de speciﬁcations et des preuves formelles ont pris de l'ampleur durant les dernieres decennies, elabores au sein d'une diversite de canevas, de systemes et de communautes. Cependant l'heterogeneite de ces environnements gene quelques-unes des etapes fondamentales du processus de reﬂexion scientiﬁque : le partage et la reutilisation des resultats. Cette dissertation propose une methode de distribution du meme developpement formel entre de divers systemes de preuve, augmentant ainsi eur interoperabilite. es chapitres 1 et 2 presentent le cadre logique qui est employe pour centraliser les speciﬁcations et les preuves formelles. Sa principale contribution est une ariation du λµ˜ µ-calcul conçu pour supporter le eveloppement interactif de preuves. Les chapitres 3 et 4 developpent les structures de recriture et categoriques necessaire a l'expression formelle de la semantique des langages de preuve. Base sur ces premiers resultats, le chapitre 5 utilise un systeme de types pour des langages de preuve pour asseoir un propriete de surete de typage, et le chapitre 6 expose une serie de traductions des developpements centralises dans d'autres cadres formels majeurs. Entre autres, le dernier contribue a une simpliﬁcation des systemes de deduction a la Frege-Hilbert. En conclusion, les chapitres 7 et 8 s'interessent aux problemes resultant de l'implementation de notre systeme de developpement centralise de preuve. Ainsi, celui-ci decrit les details du logiciel cree, et celui-la fait la presentation d'une theorie de classes qui permet l'expression ﬁnie au premier ordre de schemas d'axiomes.

Gli stili APA, Harvard, Vancouver, ISO e altri

7

Seyrat, Claude. "L' interopérabilité dans les systèmes d'indexation multimédia". Paris 6, 2003. http://www.theses.fr/2003PA066307.

Testo completo

Gli stili APA, Harvard, Vancouver, ISO e altri

8

Nowak, David. "Spécification et preuve de systèmes réactifs". Rennes 1, 1999. http://www.theses.fr/1999REN10094.

Testo completo

Abstract (sommario):

Ces dernieres annees, la verification des systemes informatiques critiques est devenue un sujet de recherche important en raison du developpement croissant de logiciels pour la medecine, les moyens de transports ou les centrales nucleaires. Dans ces domaines, une erreur de programmation peut couter tres cher financierement ou en vies humaines. Dans ce cadre, les informaticiens ont ete amenes a developper des langages dits synchrones dedies a la programmation des systemes reactifs. Un systeme reactif est un systeme qui reagit continument avec son environnement a un vitesse imposee par son environnement. Il ne termine pas forcement et peut etre concurrent. En general, la concurrence entraine le non-determinisme mais le modele synchrone se distingue par le fait qu'il fait cohabiter concurrence et determinisme. Dans cette these, nous avons formalise dans l'outil d'aide a la preuve coq une version co-inductive de la semantique des traces du langage synchrone signal. Nous avons choisi d'utiliser la co-induction car nous pensons qu'il s'agit la d'un outil mathematique naturel et simple pour manipuler des objets infinis tels que les signaux. La pratique nous permet de confirmer que la co-induction est un outil efficace pour prouver la correction d'un systeme reactif specifie en signal. Afin de pouvoir traiter la causalite dans les programmes synchrones, nous avons ensuite generalise cette approche en developpant une variante des structures d'evenements que nous appelons les structures synchrones. Par cette approche, il est possible de traiter les dependances conditionnees entres signaux et il n'est pas necessaire de denoter l'absence d'un signal par une valeur speciale comme cela est fait usuellement. C'est plus en accord avec la realite car l'absence d'un signal doit etre inferee par le programme (endochronie).

Gli stili APA, Harvard, Vancouver, ISO e altri

9

Cuggia, Marc. "Interopérabilité des systèmes d'information en santé et aspects sémantiques". Rennes 1, 2008. http://www.theses.fr/2008REN1B116.

Testo completo

Abstract (sommario):

L'interopérabilité des systèmes d'information en santé est un enjeu majeur, puisque ces systèmes sont hétérogènes tant sur leurs domaines de couvertures, leurs structures et leurs contenus. L'objectif de ce travail est d'explorer certains aspects de l'interopérabilité, en particulier sémantique. La thèse contient trois parties. (i) Un état des lieux des systèmes d'information en santé, ainsi que sur la place des normes et standards d'interopérabilité en santé. (ii) Une modélisation et mise en œuvre expérimentale d'un système d'information en santé pour un réseau de soins ville hôpitaux. (iii) L'exploration des aspects spécifiquement sémantiques, où sont abordés au travers de plusieurs études, les problématiques de liaison des modèles d'information (ici HL7, OpenEHR) avec les modèles de connaissances (ici SNOMED international, CT & LOINC)
The interoperability of health information systems is a major issue, since these systems are heterogeneous both in their areage of coverages, their structures and their contents. The objective of this work is to explore some aspects of interoperability, in particular the semantic aspects. The thesis is three parts structured. (i) An inventory of health information systems and the place of interoperability norms and standards in health domain. (ii) Modeling and experimental implementation information of a system for health care networks. (iii) Specific aspects of semantic issues are investigated through several studies, the difficulties to connect information models (HL7 here, OpenEHR) with models of knowledge (by SNOMED International, CT & LOINC)

Gli stili APA, Harvard, Vancouver, ISO e altri

10

Malet, Emmanuel. "Interopérabilité des systèmes d'IAO : les services de prototypage rapide". Reims, 2003. http://theses.univ-reims.fr/sciences/2003REIMS020.pdf.

Testo completo

Abstract (sommario):

Résumé : Dans le contexte de l'ingénierie collaborative et de l'entreprise étendue, la collaboration des différents acteurs passe par l'interopérabilité des systèmes d'IAO(Ingénierie Assistée par Ordinateur), celle-ci devant être fondée sur des solutions technologiques normalisées. Cantonnée aux échanges de fichiers suivant différents formats (IGES, SET, VDA etc. ), l'interopérabilité des systèmes CAO (Conception Assistée par Ordinateur) s'est longtemps heurtée et se heurte encore aujourd'hui à l'hétérogénéité des représentations utilisées. AU Milieu des années quatre vingts, le projet STEP (STandard for Exchange of Product data model) propose de normaliser les représentations du produit utilisées dans les divers secteurs de l'industrie pour en permettre l'échange et le partage. Vingt ans plus tard, le processus de normalisation n'est toujours pas terminé et ses retombées toujours attendues. . . Parallèlement dans le secteur des télécommunications, le problème de l'intéopérabilité logicielle se pose de manière générale : comment faire collaborer des ressources hétérogènes et distribuées ? Basée sur les concepts orientés objet d'abstraction et d'encapsulation, les architectures de médiation (CORBA, DCOM) permettent à des objets hétérogènes et distribués de collaborer au travers d'interfaces bien définies. Récemment l'OMG (Object Management Group) décide d'appliquer cette approche à l'IAO. Les services de CAO, de simulation distribuée et de GDT (Gestion de données Techniques) sont alors normalisés. A travers la présentation détaillée des normes STEP, DCOM et CORBA, cette thèse présente les différences fondamentales entre ces deux approches. Nous proposons ensuite, dans la continuité des travaux de l'OMG, de revoir l'interopérabilité entre système de CAO et système de prototypage au moyen de la médiation. Nous proposons pour cela de spécifier les interfaces d'un certain nombre de composants usuels des systèmes de prototypage : les modèles STL et STL topologique, les services de tranchage et de remplissage, traitant des cas de singularités au regard des voisinages. Enfin, nous présentons un système de prototypage rapide utilisable via Internet, développé à des fins de validation.

Gli stili APA, Harvard, Vancouver, ISO e altri

11

Bah, Abdramane. "Interopérabilité et sécurité des systèmes d'information : application aux systèmes de gestion de l'éducation". Thesis, Nantes, 2020. http://www.theses.fr/2020NANT4028.

Testo completo

Abstract (sommario):

Le contrôle d’accès des services partagés est une exigence essentielle pour une fédération de services de différents domaines. Dans cette thèse, nous nous sommes attaqués à deux problèmes de contrôle d’accès : l’autorisation des utilisateurs et la délégation de l’authentification des utilisateurs à leurs propres domaines. Pour répondre à ces problèmes, nous avons proposé une méthode d’autorisation des utilisateurs basée sur la technique de mapping d’attributs et un mécanisme de contrôle d’accès fédéré pour mettre en oeuvre cette méthode d’autorisation. Nous avons proposé une méthode de fédération services pour déléguer l’authentification des utilisateurs à leurs propres domaines. Le principal objectif est de permettre à divers domaines de collaborer malgré l’hétérogénéité de leurs modèles de sécurité
Access control for shared services is an essential requirement for a federation of services from different domains. In this thesis, we tackled two access control problems : authorizing users and delegating user authentication to their own domains. To address these problems, we have proposed a method of authorizing users based on the attribute mapping technique and a federated access control mechanism to implement this authorization method. We have proposed a service federation method to delegate user authentication to their domains. The main objective is to allow various domains to collaborate despite the heterogeneity of their security models

Gli stili APA, Harvard, Vancouver, ISO e altri

12

Mornet, Marie-Noëlle. "La preuve par vidéosurveillance". Université Robert Schuman (Strasbourg) (1971-2008), 2003. http://www.theses.fr/2003STR30007.

Testo completo

Abstract (sommario):

L'étude porte sur la recherche de la preuve et sa mise en œuvre dans un litige. Elle conduit à déterminer la réglementation de la vidéosurveillance et sa pertinence. Des critères sont communs à une utilisation licite du procédé: celui de l'information des personnes nécessaires mais insuffisant et celui de la proportionnalité permettant d'adapter l'atteinte aux droits des personnes à la nécessité de la surveillance vidéo. La divergence de jurisprudence quant à l'admissibilité de l'enregistrement vidéo et l'évaluation variable de sa force probante s'opposent au principe d'équité du procès. Des améliorations du système doivent être envisagées avec la fixation d'une limite à l'admissibilité de la preuve irrégulière et la précision des modalités d'évaluation de la force probante. Il importe aussi que le magistrat prenne en compte le critère de la proportionnalité lors de son jugement, cette attitude emportant des conséquences sur l'usage de la vidéosurveillance par les justiciables
The study discusses evidence-seeking and the way it is implemented in a legal dispute. It aims at determining the regulation with regard to closed circuit television (CCTV) and its relevance. There are common criteria for a lawfull use of the process, i-e the information of individuals which is necessary, although insufficient, and the proportionality allowing to adapt the infringement of a person's rights to the necessity of CCTV. The divergence of case law in regard to the video recordings' admissibility, and the variable valuation of the evidence's weight are against the principles of the law suit's equity. The system must be improved: a limit must be set to the admissibility of the irregular evidence and more accuracy of the clauses of valuation of the probative value is needed. Moreover, the judge should take into consideration the proportionality criterion upon his sentence. This may have consequences on the use made of CCTV by individual interests

Gli stili APA, Harvard, Vancouver, ISO e altri

13

Melliti, Tarek. "Interopérabilité des services Web Complexes : Application aux systèmes multi-agents". Paris 9, 2004. https://portail.bu.dauphine.fr/fileviewer/index.php?doc=2004PA090024.

Testo completo

Abstract (sommario):

Ce travail porte sur la formalisation de l'interopérabilité opérationnelle entre deux systèmes communicants et plus particulièrement entre les services Web composites. La formalisation retranscrit la possibilité d'une interaction correcte entre deux systèmes communicant utilisant des spécifications différentes. Cette formalisation se matérialise en trois étapes: Premièrement, nous définissons l'observabilité comme référence d'abstraction pour exprimer la sémantique de différentes spécifications. Ensuite, nous proposons une relation de conformité sur les états de deux systèmes qui retranscrit la notion d'interaction correcte. Enfin, nous définissons un algorithme de synthèse qui, étant données la spécification d'un service composite et sa sémantique observable soit génère un client correct soit détecte une ambiguïté. Le travail a donné lieu à la réalisation d'une plate-forme de gestion d'interaction pour les services composites et un environnement d'intégration de systèmes multi-agents
This work concerns the formalization of operational interoperabilility between two communicating systems and particularly between the composite services. Formalization retranscribes the possibility of a correct interaction between two communicating systems using different specifications. This formalization materializes in three steps: Firstly, we define the observability as a reference of abstraction to express the semantics of different specification. Then, we propose a relation of conformity on the states of two systems which retranscribes the concept of correct interaction. Lastly, we define a synthesis algorithm which, being given the specification of a composite service and its observable semantics, either generates a correct client or detect an ambiguous behaviour. This work lead to a realisation of a composite Web services interaction plate-form and an environment of multi-agent systems integration

Gli stili APA, Harvard, Vancouver, ISO e altri

14

Diagne, Fama. "Preuve de propriétés dynamiques en B". Phd thesis, Institut National des Télécommunications, 2013. http://tel.archives-ouvertes.fr/tel-00939071.

Testo completo

Abstract (sommario):

Les propriétés que l'on souhaite exprimer sur les applications système d'information ne peuvent se restreindre aux propriétés statiques, dites propriétés d'invariance, qui portent sur des états du système pris au même moment. En effet, certaines propriétés, dites propriétés dynamiques, peuvent faire référence à l'état passé ou futur du système. Les travaux existants sur la vérification de telles propriétés utilisent généralement le model checking dont l'efficacité pour le domaine des systèmes d'information est plutôt réduite à cause de l'explosion combinatoire de l'espace des états. Aussi, les techniques, fondées sur la preuve, requièrent des connaissances assez avancées en termes de raisonnement mathématique et sont donc difficiles à mettre en œuvre d'autant plus que ces dernières ne sont pas outillées. Pour palier ces limites, nous proposons dans cette thèse des méthodes de vérification de propriétés dynamiques basées sur la preuve en utilisant la méthode formelle B. Nous nous intéressons principalement aux propriétés d'atteignabilité et de précédence pour lesquelles nous avons défini des méthodes de génération d'obligations de preuve permettant de les prouver. Une propriété d'atteignabilité permet d'exprimer qu'il existe au moins une exécution du système qui permet d'atteindre un état cible à partir d'un état initial donné. Par contre, la propriété de précédence permet de s'assurer qu'un état donné du système est toujours précédé par un autre état. Afin de rendre ces différentes approches opérationnelles, nous avons développé un outil support qui permet de décharger l'utilisateur de la tâche de génération d'obligations de preuve qui peut être longue et fastidieuse

Gli stili APA, Harvard, Vancouver, ISO e altri

15

Baïna, Salah. "Interopérabilité dirigée par les modèles : une Approche Orientée Produit pour l'interopérabilité des systèmes d'entreprise". Nancy 1, 2006. https://tel.archives-ouvertes.fr/tel-00123271.

Testo completo

Abstract (sommario):

L’intégration des systèmes consiste à assembler les différentes parties d’un système tout en assurant la compatibilité de l’assemblage ainsi que le bon fonctionnement du système complet. Dans ce cadre, l’interopérabilité des systèmes est un moyen pour obtenir l’intégration fondée sur un couplage faible des parties du système, basé sur la capacité des parties à des parties à communiquer entre elles pour accéder et faire appel à leur fonctionnalités. Plus récemment, une nouvelle approche d’ingénierie logicielle a été élaborée «l’ingénierie dirigée par les modèles». Dans cette nouvelle approche les modèles occupent une place de premier plan parmi les artefacts d’ingénierie des systèmes. La thèse s’inscrit dans l’intersection de ces deux domaines de recherche. Dans ce contexte, les travaux de la thèse présentent une approche pour l’interopérabilité entre systèmes d’entreprise dite « l’interopérabilité orientée produit »; basée sur les échanges d’informations relatives au produit bien et service entre les différents modèles et représentation de ce produit dans chacun des systèmes. Nous proposons ainsi un meta-modèle dont les instances jouent le rôle de modèles pivot pour la communication entre différentes applications d'entreprise et ceci dans le but d’assurer l'interopérabilité des parties de systèmes concernant le produit. Pour la formalisation de ce meta-modèle, notre approche s'est inspirée sur l’ontologie BWW (Bunge - Wand - Weber) permettant la construction de représentations génériques et complètes des objets du monde réel tels que les perçoivent les systèmes d’information
Systems integration aims at assembling several systems in order to build a unique system working and reacting as a whole. In this context, systems interoperability can be seen as a means to obtain integration based on a light coupling of sub-parts of the system. Recently, a new approach of systems development based on modelling techniques has been founded. This approach is called “Model driven engineering”, in this approach models play a key role in systems engineering and development. This Phd thesis presents a product oriented approach for interoperability to ensure data and schema consistency between all product representations in a production. The aim of product oriented interoperability is, on one hand, to define mechanisms to maintain consistency between this representation and the reality of the product, and on the other hand to make sure that all applications share the image (representation) of the same product. Our result is a model driven approach based on a generic meta-model that defines all concepts used for representing the product. To enable data exchange between different applications, a formalisation of model driven mappings for semantic interoperability has also been proposed. To achieve our goal we focus on the formalisation of a unified product representation inside enterprise information systems. This unified representation has been inspired from the well know BWW ontology (Bunge - Wand - Weber) that is widely used for real world objects representation for information systems design. In this thesis, a reference meta-model has been defined, to enable structured data exchange between different applications

Gli stili APA, Harvard, Vancouver, ISO e altri

16

Lick, Anthony. "Logique de requêtes à la XPath : systèmes de preuve et pertinence pratique". Thesis, Université Paris-Saclay (ComUE), 2019. http://www.theses.fr/2019SACLN016/document.

Testo completo

Abstract (sommario):

Motivées par de nombreuses applications allant du traitement XML à lavérification d'exécution de programmes, de nombreuses logiques sur les arbresde données et les flux de données ont été développées dans la littérature.Celles-ci offrent divers compromis entre expressivité et complexitéalgorithmique ; leur problème de satisfiabilité a souvent une complexité nonélémentaire ou peut même être indécidable.De plus, leur étude à travers des approches de théories des modèles ou dethéorie des automates peuvent être algorithmiquement impraticables ou manquerde modularité.Dans une première partie, nous étudions l'utilisation de systèmes de preuvecomme un moyen modulaire de résoudre le problème de satisfiabilité des données logiques sur des structures linéaires.Pour chaque logique considérée, nous développons un calcul d'hyperséquentscorrect et complet et décrivons une stratégie de recherche de preuve optimaledonnant une procédure de décision NP.En particulier, nous présentons un fragment NP-complet de la logique temporelle sur les ordinaux avec données, la logique complète étant indécidable, qui est exactement aussi expressif que le fragment à deux variables de la logique du premier ordre sur les ordinaux avec données.Dans une deuxième partie, nous menons une étude empirique des principaleslogiques à la XPath décidables proposées dans la littérature.Nous présentons un jeu de tests que nous avons développé à cette fin etexaminons comment ces logiques pourraient être étendues pour capturer davantage de requêtes du monde réel sans affecter la complexité de leur problème de satisfiabilité.Enfin, nous analysons les résultats que nous avons recueillis à partir de notre jeu de tests et identifions les nouvelles fonctionnalités à prendre en charge afin d’accroître la couverture pratique de ces logiques
Motivated by applications ranging from XML processing to runtime verificationof programs, many logics on data trees and data streams have been developed in the literature.These offer different trade-offs between expressiveness and computationalcomplexity; their satisfiability problem has often non-elementary complexity or is even undecidable.Moreover, their study through model-theoretic or automata-theoretic approaches can be computationally impractical or lacking modularity.In a first part, we investigate the use of proof systems as a modular way tosolve the satisfiability problem of data logics on linear structures.For each logic we consider, we develop a sound and complete hypersequentcalculus and describe an optimal proof search strategy yielding an NPdecision procedure.In particular, we exhibit an NP-complete fragment of the tense logic over data ordinals---the full logic being undecidable---, which is exactly as expressive as the two-variable fragment of the first-order logic on data ordinals.In a second part, we run an empirical study of the main decidable XPath-likelogics proposed in the literature.We present a benchmark we developed to that end, and examine how these logicscould be extended to capture more real-world queries without impacting thecomplexity of their satisfiability problem.Finally, we discuss the results we gathered from our benchmark, and identifywhich new features should be supported in order to increase the practicalcoverage of these logics

Gli stili APA, Harvard, Vancouver, ISO e altri

17

Sioud, Esma. "Contribution à l'évaluation de l'interopérabilité sémantique entre systèmes d'information d'entreprises : application aux systèmes d'information de pilotage de la production". Thesis, Nancy 1, 2011. http://www.theses.fr/2011NAN10049/document.

Testo completo

Abstract (sommario):

Les travaux présentés dans ce mémoire s'inscrivent dans le contexte de systèmes d'entreprises collaboratives. Nous défendons l'intérêt d'évaluer l'interopérabilité étant donné que la question de l'interopérabilité voire plutôt celle de la non-interopérabilité pose de nombreuses problématiques pour les industriels. En effet, la non-interopérabilité engendre des coûts non négligeables dus principalement au temps et aux ressources mises en place pour développer des interfaces d'échange des informations. Ceci influe sur la performance globale des entreprises et précisément sur les coûts et les délais d'obtention des services attendus. Nous proposons ainsi une approche pour mesurer, a priori, le degré d'interopérabilité (ou de non interopérabilité) entre modèles conceptuels de systèmes d'information d'entreprise, afin de donner à une entreprise la possibilité d'évaluer sa propre capacité à interopérer et donc de prévoir les éventuels problèmes avant la mise en place d'un partenariat. Il s'agit ainsi de définir des indicateurs et des métriques tant quantitatifs que qualitatifs, permettant de qualifier l'interopérabilité entre les systèmes d'entreprises et de proposer des stratégies d'amélioration lorsque le niveau d'interopérabilité est évalué comme insuffisant
Within the context of collaborative enterprise information systems, these works aim to propose an approach for assessing the interoperability and the non-interoperability. In fact, the non-interoperability poses a series of challenging problems to the industrial community. Indeed, the non-interoperability leads to significant costs. The majority of these costs are attributable to the time and resources spent to put in place interfaces for exchanging information. This mainly affects enterprise global performance by increasing the cost and the delay to obtain the expected services. We suggest to address enterprise interoperability measurement in order to allow to any enterprise to fully evaluate, a priori, its own capacity to interoperate, and therefore to anticipate possible problems before a partnership. Our works consist in defining indicators and metrics to quantify and then to qualify the interoperability between the enterprise systems and to propose some improvement strategies when the evaluated interoperability level is not sufficient

Gli stili APA, Harvard, Vancouver, ISO e altri

18

Yahia, Esma. "Contribution à l'évaluation de l'interopérabilité sémantique entre systèmes d'information d'entreprise : Application aux systèmes d'information de pilotage de la production". Phd thesis, Université Henri Poincaré - Nancy I, 2011. http://tel.archives-ouvertes.fr/tel-00630118.

Testo completo

Abstract (sommario):

Les travaux présentés dans ce mémoire s'inscrivent dans le contexte de systèmes d'entreprises collaboratives. Nous défendons l'intérêt d'évaluer l'interopérabilité étant donné que la question de l'interopérabilité voire plutôt celle de la non-interopérabilité pose de nombreuses problématiques pour les industriels. En effet, la non-interopérabilité engendre des coûts non négligeables dus principalement au temps et aux ressources mises en place pour développer des interfaces d'échange des informations. Ceci influe sur la performance globale des entreprises et précisément sur les coûts et les délais d'obtention des services attendus. Nous proposons ainsi une approche pour mesurer, a priori, le degré d'interopérabilité (ou de non interopérabilité) entre modèles conceptuels de systèmes d'information d'entreprise, afin de donner à une entreprise la possibilité d'évaluer sa propre capacité à interopérer et donc de prévoir les éventuels problèmes avant la mise en place d'un partenariat. Il s'agit ainsi de définir des indicateurs et des métriques tant quantitatifs que qualitatifs, permettant de qualifier l'interopérabilité entre les systèmes d'entreprises et de proposer des stratégies d'amélioration lorsque le niveau d'interopérabilité est évalué comme insuffisant.

Gli stili APA, Harvard, Vancouver, ISO e altri

19

François, Axel. "Interopérabilité des modèles géométriques pour les Systèmes d'Information Géographique : applications de la norme ISO 19107". Thesis, Aix-Marseille 2, 2011. http://www.theses.fr/2011AIX22078/document.

Testo completo

Abstract (sommario):

Le contexte économique actuel montre que la représentation et l'analyse des données dans l'espace 3D croît de plus en plus dans les Systèmes d'Information Géographique (SIG). Le nombre d'applications SIG est en constante augmentation dans de nombreux secteurs d'activités comme par exemple la Défense, l'Aménagement du Territoire ou la Sécurité Civile. Cependant, nous voyons l'émergence d'une forte demande pour l'analyse 3D dans les SIG. Ces développements nécessitent une standardisation des structures de données et d'échanges. Cette démarche est réalisée par l'Open Geospatial Consortium (OGC) et l'organisation internationale de normalisation (ISO). Une norme récente (ISO 19107:2003) décrit les objets complexes à prendre en compte et les traitements qu’il est possible de leur appliquer. Elle cherche à mettre en place l’interopérabilité des échanges et des analyses de données géométriques et topologiques dans les SIG. Actuellement aucune implémentation informatique complète de cette norme n’a été encore réalisée, compte tenu de son niveau d'abstraction. Une version simplifiée a toutefois été développée pour des objets uniquement 2D (ISO 19137:2007). Ce travail de thèse propose la modélisation et l’analyse d'objets complexes dans un espace tridimensionnel, et les traitements associés pour réaliser une première bibliothèque de fonctionnalités conforme à la norme ISO 19107. De plus, cette norme est actuellement portée en révision au sein du consortium OGC (Open Geospatial Consortium, www.opengeospatial.org) avec une nécessité de correction et d’évolution. Les travaux menés jusqu'à présent ont permis d’apporter une contribution pertinente avec l'ajout de nouvelles primitives géométriques, l'harmonisation de primitives par l'usage de courbes et surfaces paramétriques rationnelles. Les travaux sur cette norme ont permis également l’élaboration d'une application au sein de la société GEOMATYS, rendant possible la modélisation et l'analyse 3D d'un trafic aérien reposant sur des données SIG
In the current economic context, the representation and the analysis of 3D data is growing more and more in the field of Geographic Information Systems (GIS). The number of GIS applications is constantly increasing in many industries, such as Defense, Regional Development and Civil Security. However, we can point out the emergence of an important request for 3D analysis in GIS. These developments require a standardization of data and exchange structures. This is carried out by Open Geospatial Consortium (OGC) and International Organization for Standardization (ISO). A recent standard (ISO 19107:2003) describes the complex objects to be taken into consideration and the associated treatments that can be used. It aims to develop interoperable exchange and analysis of geometric and topological data in GIS. Currently, no complete implementation on a computer of this standard has been done yet, regarding the level of abstraction sought. However, a simplified version was exclusively developed for 2D objects (ISO 19137:2007). This thesis proposes the modeling and the analysis of complex objects in three dimensional space, with their associated treatments. The objective is to create a first library whose the features are conform to ISO19107. Moreover, this standard is currently under review within the OGC Consortium (Open Geospatial Consortium) with a need for correction and evolution. The work done until now have enabled us to make a meaningful contribution with the addition of new geometrical primitives, the harmonization of primitives through the use of rational parametric curves and surfaces. The works on this standard also allowed the development of an application within the GEOMATYS company, making possible the 3D modeling and analysis for traffic simulation based on GIS data

Gli stili APA, Harvard, Vancouver, ISO e altri

20

Bondé, Lossan. "Transformations de modèles et interopérabilité dans la conception de systèmes hétérogènes sur puce à base d'IP". Lille 1, 2006. https://pepite-depot.univ-lille.fr/LIBRE/Th_Num/2006/50376-2006-Bonde.pdf.

Testo completo

Abstract (sommario):

Un système sur puce (SoC, pour« System on Chip ») est un circuit intégré qui comporte un ensemble de composants matériels (microprocesseurs, DSP, entrées/sorties. . . ) connectés entre eux par des bus de communication et une couche logicielle (système d'exploitation temps réel et applicatif). La conception de tels systèmes repose de plus en plus sur la réutilisation de composants virtuels (IP, pour Intellectual property). Le concepteur utilise des IPs très souvent d'origines diverses ayant des modèles hétérogènes (différents niveaux d'abstraction : comportemental, RTL, etc. ). Cette approche améliore le délai de mise sur le marché («time to market»), mais elle nécessite de la part du concepteur de nouvelles méthodes de conception. Gaspard propose une méthodologie basée sur l'Ingénierie Dirigée par les modèles (IDM) pour la conception des SoCs. Il vise l'utilisation de plusieurs plates-formes de simulation (Java, OpenMP, SystemC, VHDL, etc. ) et différents niveaux d'abstraction (TLM, RTL, etc. ). Les modèles des différentes plates-formes et niveaux d'abstraction sont générés dans Gaspard par transformations de modèles. L'hétérogénéité des plates-formes visées introduit un problème d'interopérabilité. Dans ce travail de thèse, nous proposons une démarche basée sur l'IDM pour répondre à ce besoin d'interopérabilité. Cette solution est élaborée en trois étapes. Dans un premier temps, nous introduisons la traçabilité dans les transformations de modèles; un modèle de trace est alors généré pendant les phases de transformations de modèles. Ce modèle de trace est ensuite utilisé en entrée d'une transformation pour générer un modèle de pont («bridge») d'interopérabilité. Enfin, la génération du code du pont d'interopérabilité est réalisée à partir du modèle de pont. Pour automatiser ce processus, nous avons défini un métamodèle de traçabilité et un métamodèle de pont d'interopérabilité. Les différentes opérations de transformations de modèles nécessaires ont également été décrites.

Gli stili APA, Harvard, Vancouver, ISO e altri

21

Nguyen, Quang Huy. "Calcul de réécriture et automatisation du raisonnement dans les assistants de preuve". Nancy 1, 2002. http://www.theses.fr/2002NAN10144.

Testo completo

Abstract (sommario):

Nous étudions dans cette thèse une coopération entre la réécriture du premier ordre et la théorie constructive des types pour automatiser les preuves assistées par l'ordinateur. Nous cherchons par ce travail à mettre en oeuvre la réécriture de manière automatique, sûre et efficace dans l'assistant de preuve Coq à l'aide d'un environnement de programmation externe (ELAN). Deux approches différentes sont étudiées. Dans l'approche mixte, ELAN est utilisé comme un moteur de réécriture externe pour la normalisation des termes dans une tactique réflexive de réécriture en Coq. La trace générée par ELAN de la normalisation est rejouée en Coq pour calculer la forme normale. Afin d'améliorer la performance de la tactique réflexive, nous montrons comment utiliser la réécriture paresseuse pour obtenir une meilleure trace de normalisation. La deuxième approche, appelée externe, est plus flexible car d'une part, elle permet d'obtenir également plusieurs extensions utiles de la réécriture telles que la réécriture conditionnelle ou bien la réécriture modulo l'associativité et la commutativité (AC), et d'autre part, elle peut être facilement adaptée pour d'autres assistants de preuve. Dans cette approche, la réécriture est effectuée entièrement en ELAN et les assistants de preuve ne servent qu'à la vérifier. Nous formalisons donc la notion de terme de preuve des calculs ELAN dans le calcul de réécriture avec substitutions explicites. Nous étudions les propriétés des termes de preuve et les traduisons en syntaxe de l'assistant de preuve pour vérifier les calculs correspondants. Par conséquent, les calculs non-déterministes en ELAN peuvent être certifiés indépendamment, et nous disposons de la réécriture dans l'assistant de preuve. Afin d'améliorer la performance de la vérification des calculs concernant la réécriture modulo AC, nous proposons également une méthode de preuve efficace pour les égalités modulo AC en se basant sur la syntaxicité des théories AC. Ces résultats ont été intégrés dans une nouvelle tactique de réécriture ELAN en Coq
In this thesis, we are interested in the cooperation of first-order rewriting and constructive type theory to improve the automation of computer-aided proofs. We aim to integrate (simple, conditional or AC) rewriting in the Coq proof assistant by an automatic, safe and efficient means using an external programming environment ELAN. Two different approaches are investigated. In the mixed approach, ELAN is used as an external rewriting engine for normalising terms in a reflexive rewriting tactic in Coq. The normalisation trace generated by ELAN is replayed in Coq to compute the corresponding normal form. In order to improve the performance of this reflexive tactic, we show how to use lazy rewriting for producing compact normalisation traces. The second approach called external is more flexible since it also covers several useful extensions of term rewriting such as conditional rewriting and AC rewriting, and it can be easily adapted to other proof assistants. In this approach, term rewriting is entirely performed in ELAN and proof assistants are only used for checking purpose. We formalise the notion of proof term for ELAN computations in the rewriting calculus with explicit substitutions. We investigate the equivalent properties of the proof terms and translate them into the syntax of proof assistant in order to check the corresponding computations. By this work, non-deterministic ELAN computations can be independently certified and we obtain term rewriting in proof assistant. In order to speed up proof-checking of the computations involving AC rewriting, we also propose an efficient method for proving equalities modulo AC based on the syntacticness of AC theories. These results have been integrated in a new ELAN-based rewriting tactic in Coq

Gli stili APA, Harvard, Vancouver, ISO e altri

22

Choquer, Marie-Anne. "Preuve de formules conditionnelles dans des spécifications algébriques conditionnelles". Paris 11, 1986. http://www.theses.fr/1986PA112335.

Testo completo

Abstract (sommario):

Dans cette thèse, différentes méthodes de preuve automatique de théorèmes, définies dans le contexte des spécifications algébriques, sont résumées. Il est montré comment étendre une de ces méthodes, (la méthode par récurrence-surréduction) à la preuve de formules conditionnelles dans des spécifications algébriques conditionnelles. Cette méthode s'applique uniquement sur des spécifications satisfaisant la propriété de complétude suffisante par rapport aux constructeurs. Cette propriété est donc étudiée pour le cas des spécifications conditionnelles
In this thesis, different proof methods in algebraic specifications are outlined. One of them (the induction-narrowing method) is extended to prove conditional formulas in conditional specifications. This method can only be applied on specifications satisfying the property of sufficient completness with respect to the constructors. This property is studied for conditional specifications

Gli stili APA, Harvard, Vancouver, ISO e altri

23

Gaaloul, Sana. "Interopérabilité basée sur les standards Modelica et composant logiciel pour la simulation énergétique des systèmes de bâtiment". Phd thesis, Université de Grenoble, 2012. http://tel.archives-ouvertes.fr/tel-00782540.

Testo completo

Abstract (sommario):

Pour mieux maîtriser ses flux énergétiques et respecter les diverses restrictions mises en place dans ce secteur énergivore, le bâtiment devient un système de plus en plus complexe incluant divers technologies innovantes comme les systèmes de gestion énergétiques (SGEB), une isolation performante et intégrant les énergies renouvelables. Cette complexité exige un changement dans les techniques et paradigmes actuels de simulation du bâtiment pour la prise en compte de ses diverses évolutions. Une modélisation globale des différents composants de ce système et une simulation efficace de ses sous-systèmes hétérogènes doivent être dorénavant assurées. Ces objectifs ne pourront être atteints qu'à travers l'exploitation des approches méthodologiques d'interopérabilité. Plusieurs solutions d'interopérabilités ont été exploitées dans le secteur du bâtiment. L'état de l'art dans ce secteur, met l'accent sur le manque de standardisation des solutions appliquées. Une approche boîte blanche se basant sur le langage Modelica a remarquablement émergée. Pour monter ses intérêts ainsi que ses limites, cette solution est adoptée pour la modélisation du système de bâtiment "PREDIS", à haute performance énergétique. Une approche boîte noire complémentaire, s'appuyant sur le standard de composant logiciel dédié à la simulation, est également mise en ouvre pour palier aux difficultés rencontrées en utilisant la première approche de modélisation système. Cette approche s'articule autour du concept de bus à composants permettant une interopérabilité effective entre outils de modélisation et environnements de simulation. En plus de l'architecture logicielle autour de la plateforme d'interopérabilité, une simulation efficace du système hétérogène requière des techniques de simulations adaptées. Ces dernières peuvent exiger des adaptations des modèles utilisés qui sont prévues par la norme de composant.

Gli stili APA, Harvard, Vancouver, ISO e altri

24

Baïna, Salah. "INTEROPERABILITE DIRIGEE PAR LES MODELES :Une Approche Orientée Produit pour l'interopérabilité dessystèmes d'entreprise". Phd thesis, Université Henri Poincaré - Nancy I, 2006. http://tel.archives-ouvertes.fr/tel-00123271.

Testo completo

Abstract (sommario):

Les travaux de la thèse présentent une approche pour l'interopérabilité entre les différents
modèles de produit, nous appellerons cette approche « l'interopérabilité orientée produit ».
Nous proposons ainsi un meta-modèle dont les instances jouent le rôle de passerelle de
communication entre différentes applications d'entreprise pour assurer l'interopérabilité des
parties de systèmes concernant le produit.
Nous nous sommes intéressés à formaliser un meta-modèle pour la définition du concept de
produit comme l'agrégation d'une partie physique représentant les éléments physiques du
produit et une partie informationnelle reprenant les éléments informationnels décrivant le
produit.
L'outillage et le prototypage du concept de produit holonique lors de la modélisation du
processus de fabrication dans l'entreprise ainsi que la prise en charge des mapping pour
l'interopérabilité s'appuient sur l'intégration du meta-modèle holonique dans un
environnement de modélisation d'entreprise particulier.
La phase de validation a été réalisée en deux parties représentées chacune par une application
industrielle. La première application se situe dans le cadre d'une collaboration avec le
département meunerie dans un grand groupe industriel, pour une application en
environnement réel de la modélisation holonique. L'objectif de cette application est de
concevoir un système de traçabilité pour les différents produits par les moulins du groupe.
Notre participation dans ce projet, a consisté en l'application de l'approche de modélisation
holonique pour la spécification, a priori, de l'ensemble des données et informations relatives
aux produits devant être prises en compte dans le système de traçabilité, et ainsi de générer de
manière automatique le schéma de données préliminaire du système. La seconde application
concerne la mise en œuvre de l'approche holonique pour une solution d'interopérabilité
orienté produit dans le cadre du pôle AIP Lorrain (AIPL).

Gli stili APA, Harvard, Vancouver, ISO e altri

25

Jomaa, Narjes. "Le co-design d’un noyau de système d’exploitation et de sa preuve formelle d’isolation". Thesis, Lille 1, 2018. http://www.theses.fr/2018LIL1I075/document.

Testo completo

Abstract (sommario):

Dans cette thèse nous proposons un nouveau concept de noyau adapté à la preuve que nous avons appelé « proto-noyau ». Il s’agit d’un noyau de système d’exploitation minimal où la minimisation de sa taille est principalement motivée par la réduction du coût de la preuve mais aussi de la surface d’attaque. Ceci nous amène à définir une nouvelle stratégie de « co-design » du noyau et de sa preuve. Elle est fondée principalement sur les feedbacks entre les différentes phases de développement du noyau, allant de la définition des besoins jusqu’à la vérification formelle de ses propriétés. Ainsi, dans ce contexte nous avons conçu et implémenté le proto-noyau Pip. L’ensemble de ses appels système a été choisi minutieusement pendant la phase de conception pour assurer à la fois la faisabilité de la preuve et l’utilisabilité du système. Le code de Pip est écrit en Gallina (le langage de spécification de l’assistant de preuve Coq) puis traduit automatiquement vers le langage C. La propriété principale étudiée dans ces travaux est une propriété de sécurité, exprimée en termes d’isolation mémoire. Cette propriété a été largement étudiée dans la littérature de par son importance. Ainsi, nos travaux consistent plus particulièrement à orienter le développement des concepts de base de ce noyau minimaliste par la vérification formelle de cette propriété. La stratégie de vérification a été expérimentée, dans un premier temps, sur un modèle générique de micro-noyau que nous avons également écrit en Gallina. Par ce modèle simplifié de micro-noyau nous avons pu valider notre approche de vérification avant de l’appliquer sur l’implémentation concrète du proto-noyau Pip
In this thesis we propose a new kernel concept adapted to verification that we have called protokernel. It is a minimal operating system kernel where the minimization of its size is motivated by the reduction of the cost of proof and of the attack surface. This leads us to define a new strategy of codesign of the kernel and its proof. It is based mainly on the feedbacks between the various steps of development of the kernel, ranging from the definition of its specification to the formal verification of its properties. Thus, in this context we have designed and implemented the Pip protokernel. All of its system calls were carefully identified during the design step to ensure both the feasibility of proof and the usability of the system. The code of Pip is written in Gallina (the specification language of the Coq proof assistant) and then automatically translated into C code. The main property studied in this work is a security property, expressed in terms of memory isolation. This property has been largely discussed in the literature due to its importance. Thus, our work consists more particularly in guiding the developer to define the fundamental concepts of this minimalistic kernel through the formal verification of its isolation property. The verification strategy was first experimented with a generic microkernel model that we also wrote in Gallina. With this simplified microkernel model we were able to validate our verification approach before applying it to the concrete implementation of the Pip protokernel

Gli stili APA, Harvard, Vancouver, ISO e altri

26

Xu, Yigang. "Une architecture de médiation basée sur des composants génériques pour l'intégration des systèmes d'information de santé". Paris 6, 2002. http://www.theses.fr/2002PA066376.

Testo completo

Gli stili APA, Harvard, Vancouver, ISO e altri

27

Sioud, Esma. "Contribution à l'évaluation de l'interopérabilité sémantique entre systèmes d'information d'entreprises : application aux systèmes d'information de pilotage de la production". Electronic Thesis or Diss., Nancy 1, 2011. http://www.theses.fr/2011NAN10049.

Testo completo

Abstract (sommario):

Les travaux présentés dans ce mémoire s'inscrivent dans le contexte de systèmes d'entreprises collaboratives. Nous défendons l'intérêt d'évaluer l'interopérabilité étant donné que la question de l'interopérabilité voire plutôt celle de la non-interopérabilité pose de nombreuses problématiques pour les industriels. En effet, la non-interopérabilité engendre des coûts non négligeables dus principalement au temps et aux ressources mises en place pour développer des interfaces d'échange des informations. Ceci influe sur la performance globale des entreprises et précisément sur les coûts et les délais d'obtention des services attendus. Nous proposons ainsi une approche pour mesurer, a priori, le degré d'interopérabilité (ou de non interopérabilité) entre modèles conceptuels de systèmes d'information d'entreprise, afin de donner à une entreprise la possibilité d'évaluer sa propre capacité à interopérer et donc de prévoir les éventuels problèmes avant la mise en place d'un partenariat. Il s'agit ainsi de définir des indicateurs et des métriques tant quantitatifs que qualitatifs, permettant de qualifier l'interopérabilité entre les systèmes d'entreprises et de proposer des stratégies d'amélioration lorsque le niveau d'interopérabilité est évalué comme insuffisant
Within the context of collaborative enterprise information systems, these works aim to propose an approach for assessing the interoperability and the non-interoperability. In fact, the non-interoperability poses a series of challenging problems to the industrial community. Indeed, the non-interoperability leads to significant costs. The majority of these costs are attributable to the time and resources spent to put in place interfaces for exchanging information. This mainly affects enterprise global performance by increasing the cost and the delay to obtain the expected services. We suggest to address enterprise interoperability measurement in order to allow to any enterprise to fully evaluate, a priori, its own capacity to interoperate, and therefore to anticipate possible problems before a partnership. Our works consist in defining indicators and metrics to quantify and then to qualify the interoperability between the enterprise systems and to propose some improvement strategies when the evaluated interoperability level is not sufficient

Gli stili APA, Harvard, Vancouver, ISO e altri

28

Diebold, Morgane. "Systèmes composites organogélateurs/polymères semi-conducteurs : de la preuve conceptuelle aux matériaux nanostructurés pour l'électronique plastique". Thesis, Strasbourg, 2018. http://www.theses.fr/2018STRAE002.

Testo completo

Abstract (sommario):

L’amélioration des performances des dispositifs photovoltaïques organiques passe par le contrôle de la morphologie de leurs couches actives. Nous avons cherché à préparer une hétérojonction volumique donneur-accepteur nanostructurée en utilisant la nucléation hétérogène du poly (3-hexylthiophène) (P3HT, donneur) par des fibres d’organogélateurs à base de naphthalène diimide (NDI, accepteur). La première partie de ce travail présente l’étude des propriétés d’auto-assemblage d’organogélateurs à cœur NDI substitué par des groupements amides et des dendrons trialkoxyphényles. Nous avons évalué l’influence de la longueur de la chaîne flexible entre le cœur naphthalène et les groupements amides (2 liaisons C-C pour NDI2 et 4 pour NDI4) sur les propriétés physico-chimiques des organogélateurs. La seconde partie de ce travail met en évidence le polymorphisme du composé NDI2 en identifiant 4 polymorphes ainsi que leurs signatures optiques, spectroscopiques et structurales. Un diagramme de phase de l’état solide du NDI2 est proposé. La dernière partie de la thèse concerne l’élaboration de nano-composites donneur-accepteur entre les organogélateurs à cœur NDI et le P3HT. Le processus de formation en solution de ces nano-composites est analysé en suivant les cinétiques de cristallisation du P3HT par spectroscopie d’absorption UV-Visible et les morphologies obtenues (structures shish-kebab) par microscopie électronique en transmission. L’effet nucléant des organogélateurs sur le P3HT a été montré. Les études en cellules solaires des composés P3HT:PCBM : organogélateur ont prouvé que le rendement de conversion énergétique peut être augmenté en présence d’organogélateurs
Improving the performances of organic photovoltaic devices requires morphology control of the active layers. Highly nanostructured donor-acceptor bulk heterojunctions were prepared by heterogeneous nucleation of poly (3-hexylthiophene) (P3HT, donor) on naphthalene diimide organogelators fibers (NDI, acceptor). The first part of this work was dedicated to the self-assembly of NDI-core organogelators substituted by amide groups and trialkoxyphenyls dendrons. We evaluated the influence of the flexible chain between the naphthalene core and the amide groups (2 C-C bonds for NDI2 and 4 for NDI4) on the physico-chemical properties of the organogelators.The second part of this work focused on the polymorphism of NDI2 with identification of four different polymorphs with their optical, spectroscopic and structural signatures. A phase diagram of NDI2 in the solid state was determined. The last part of this manuscript concerns the fabrication of donor-acceptor nano-composites between NDI organogelators and P3HT. The formation process in solution of these nano-composites was analyzed by following the crystallization kinetics of P3HT by UV-Vis absorption spectroscopy and the thin film morphology (shish-kebab structures) by transmission electron microscopy. The nucleating effect of various organogelators on P3HT was demonstrated. Solar cells were made from the composites P3HT:PCBM : organogelator and their energetic conversion yield was shown to be increased in the presence of organogelators

Gli stili APA, Harvard, Vancouver, ISO e altri

29

Liao, Yongxin. "Annotations sémantiques pour l'intéropérabilité des systèmes dans un environnement PLM". Thesis, Université de Lorraine, 2013. http://www.theses.fr/2013LORR0135/document.

Testo completo

Abstract (sommario):

Dans l'industrie l'approche de gestion du cycle de vie du produit (PLM) a été considérée comme une solution essentielle pour améliorer la compétitivité des produits. Elle vise à fournir une plate-forme commune qui rassemble les différents systèmes de l'entreprise à chaque étape du cycle de vie du produit dans ou à travers les entreprises. Bien que les principaux éditeurs de logiciels fassent des efforts pour créer des outils offrant un ensemble complet et intégré de systèmes, la plupart d' entre eux n'intègrent pas l'ensemble des systèmes. Enfin, ils ne fournissent pas une intégration cohérente de l'ensemble du système d'information. Il en résulte une sorte de « tour de Babel », où chaque application est considérée comme une île au milieu de l'océan de l'information, gérée par de nombreuses parties prenantes dans une entreprise, ou même dans un réseau d'entreprises. L'hétérogénéité des parties prenantes augmente le problème d'interopérabilité. L'objectif de cette thèse est de traiter la question de l'interopérabilité sémantique, en proposant une méthode d'annotation sémantique formelle pour favoriser la compréhension mutuelle de la sémantique de l'information partagée et échangée dans un environnement PLM
In manufacturing enterprises the Product Lifecycle Management (PLM) approach has been considered as an essential solution for improving the product competitive ability. It aims at providing a shared platform that brings together different enterprise systems at each stage of a product life cycle in or across enterprises. Although the main software companies are making efforts to create tools for offering a complete and integrated set of systems, most of them have not implemented all of the systems. Finally, they do not provide a coherent integration of the entire information system. This results in a kind of "tower of Babel", where each application is considered as an island in the middle of the ocean of information, managed by many stakeholders in an enterprise, or even in a network of enterprises. The different peculiarities of those stakeholders are then over increasing the issue of interoperability. The objective of this thesis is to deal with the issue of semantic interoperability, by proposing a formal semantic annotation method to support the mutual understanding of the semantics inside the shared and exchanged information in a PLM environment

Gli stili APA, Harvard, Vancouver, ISO e altri

30

Belghaouti, Fethi. "Interopérabilité des systèmes distribués produisant des flux de données sémantiques au profit de l'aide à la prise de décision". Thesis, Université Paris-Saclay (ComUE), 2017. http://www.theses.fr/2017SACLL003.

Testo completo

Abstract (sommario):

Internet est une source infinie de données émanant de sources telles que les réseaux sociaux ou les capteurs (domotique, ville intelligente, véhicule autonome, etc.). Ces données hétérogènes et de plus en plus volumineuses, peuvent être gérées grâce au web sémantique, qui propose de les homogénéiser et de les lier et de raisonner dessus, et aux systèmes de gestion de flux de données, qui abordent essentiellement les problèmes liés au volume, à la volatilité et à l’interrogation continue. L’alliance de ces deux disciplines a vu l’essor des systèmes de gestion de flux de données sémantiques RSP (RDF Stream Processing systems). L’objectif de cette thèse est de permettre à ces systèmes, via de nouvelles approches et algorithmes à faible coût, de rester opérationnels, voire plus performants, même en cas de gros volumes de données en entrée et/ou de ressources système limitées.Pour atteindre cet objectif, notre thèse s’articule principalement autour de la problématique du : "Traitement de flux de données sémantiques dans un contexte de systèmes informatiques à ressources limitées". Elle adresse les questions de recherche suivantes : (i) Comment représenter un flux de données sémantiques ? Et (ii) Comment traiter les flux de données sémantiques entrants, lorsque leurs débits et/ou volumes dépassent les capacités du système cible ?Nous proposons comme première contribution une analyse des données circulant dans les flux de données sémantiques pour considérer non pas une succession de triplets indépendants mais plutôt une succession de graphes en étoiles, préservant ainsi les liens entre les triplets. En utilisant cette approche, nous avons amélioré significativement la qualité des réponses de quelques algorithmes d’échantillonnage bien connus dans la littérature pour le délestage des flux. L’analyse de la requête continue permet d’optimiser cette solution en repèrant les données non pertinentes pour être délestées les premières. Dans la deuxième contribution, nous proposons un algorithme de détection de motifs fréquents de graphes RDF dans les flux de données RDF, appelé FreGraPaD (Frequent RDF Graph Patterns Detection). C’est un algorithme en une passe, orienté mémoire et peu coûteux. Il utilise deux structures de données principales un vecteur de bits pour construire et identifier le motif de graphe RDF assurant une optimisation de l’espace mémoire et une table de hachage pour le stockage de ces derniers. La troisième contribution de notre thèse consiste en une solution déterministe de réduction de charge des systèmes RSP appelée POL (Pattern Oriented Load-shedding for RDF Stream Processing systems). Elle utilise des opérateurs booléens très peu coûteux, qu’elle applique aux deux motifs binaires construits de la donnée et de la requête continue pour déterminer et éjecter celle qui est non-pertinente. Elle garantit un rappel de 100%, réduit la charge du système et améliore son temps de réponse. Enfin, notre quatrième contribution est un outil de compression en ligne de flux RDF, appelé Patorc (Pattern Oriented Compression for RSP systems). Il se base sur les motifs fréquents présents dans les flux qu’il factorise. C’est une solution de compression sans perte de données dont l’interrogation sans décompression est très envisageable. Les solutions apportées par cette thèse permettent l’extension des systèmes RSP existants en leur permettant le passage à l’échelle dans un contexte de Bigdata. Elles leur permettent ainsi de manipuler un ou plusieurs flux arrivant à différentes vitesses, sans perdre de leur qualité de réponse et tout en garantissant leur disponibilité au-delà même de leurs limites physiques. Les résultats des expérimentations menées montrent que l’extension des systèmes existants par nos solutions améliore leurs performances. Elles illustrent la diminution considérable de leur temps de réponse, l’augmentation de leur seuil de débit de traitement en entrée tout en optimisant l’utilisation de leurs ressources systèmes
Internet is an infinite source of data coming from sources such as social networks or sensors (home automation, smart city, autonomous vehicle, etc.). These heterogeneous and increasingly large data can be managed through semantic web technologies, which propose to homogenize, link these data and reason above them, and data flow management systems, which mainly address the problems related to volume, volatility and continuous querying. The alliance of these two disciplines has seen the growth of semantic data stream management systems also called RSP (RDF Stream Processing Systems). The objective of this thesis is to allow these systems, via new approaches and "low cost" algorithms, to remain operational, even more efficient, even for large input data volumes and/or with limited system resources.To reach this goal, our thesis is mainly focused on the issue of "Processing semantic data streamsin a context of computer systems with limited resources". It directly contributes to answer the following research questions : (i) How to represent semantic data stream ? And (ii) How to deal with input semantic data when their rates and/or volumes exceed the capabilities of the target system ?As first contribution, we propose an analysis of the data in the semantic data streams in order to consider a succession of star graphs instead of just a success of andependent triples, thus preserving the links between the triples. By using this approach, we significantly impoved the quality of responses of some well known sampling algoithms for load-shedding. The analysis of the continuous query allows the optimisation of this solution by selection the irrelevant data to be load-shedded first. In the second contribution, we propose an algorithm for detecting frequent RDF graph patterns in semantic data streams.We called it FreGraPaD for Frequent RDF Graph Patterns Detection. It is a one pass algorithm, memory oriented and "low-cost". It uses two main data structures : A bit-vector to build and identify the RDF graph pattern, providing thus memory space optimization ; and a hash-table for storing the patterns.The third contribution of our thesis consists of a deterministic load-shedding solution for RSP systems, called POL (Pattern Oriented Load-shedding for RDF Stream Processing systems). It uses very low-cost boolean operators, that we apply on the built binary patterns of the data and the continuous query inorder to determine which data is not relevant to be ejected upstream of the system. It guarantees a recall of 100%, reduces the system load and improves response time. Finally, in the fourth contribution, we propose Patorc (Pattern Oriented Compression for RSP systems). Patorc is an online compression toolfor RDF streams. It is based on the frequent patterns present in RDF data streams that factorizes. It is a data lossless compression solution whith very possible querying without any need to decompression.This thesis provides solutions that allow the extension of existing RSP systems and makes them able to scale in a bigdata context. Thus, these solutions allow the RSP systems to deal with one or more semantic data streams arriving at different speeds, without loosing their response quality while ensuring their availability, even beyond their physical limitations. The conducted experiments, supported by the obtained results show that the extension of existing systems with the new solutions improves their performance. They illustrate the considerable decrease in their engine’s response time, increasing their processing rate threshold while optimizing the use of their system resources

Gli stili APA, Harvard, Vancouver, ISO e altri

31

Belghaouti, Fethi. "Interopérabilité des systèmes distribués produisant des flux de données sémantiques au profit de l'aide à la prise de décision". Electronic Thesis or Diss., Université Paris-Saclay (ComUE), 2017. http://www.theses.fr/2017SACLL003.

Testo completo

Abstract (sommario):

Internet est une source infinie de données émanant de sources telles que les réseaux sociaux ou les capteurs (domotique, ville intelligente, véhicule autonome, etc.). Ces données hétérogènes et de plus en plus volumineuses, peuvent être gérées grâce au web sémantique, qui propose de les homogénéiser et de les lier et de raisonner dessus, et aux systèmes de gestion de flux de données, qui abordent essentiellement les problèmes liés au volume, à la volatilité et à l’interrogation continue. L’alliance de ces deux disciplines a vu l’essor des systèmes de gestion de flux de données sémantiques RSP (RDF Stream Processing systems). L’objectif de cette thèse est de permettre à ces systèmes, via de nouvelles approches et algorithmes à faible coût, de rester opérationnels, voire plus performants, même en cas de gros volumes de données en entrée et/ou de ressources système limitées.Pour atteindre cet objectif, notre thèse s’articule principalement autour de la problématique du : "Traitement de flux de données sémantiques dans un contexte de systèmes informatiques à ressources limitées". Elle adresse les questions de recherche suivantes : (i) Comment représenter un flux de données sémantiques ? Et (ii) Comment traiter les flux de données sémantiques entrants, lorsque leurs débits et/ou volumes dépassent les capacités du système cible ?Nous proposons comme première contribution une analyse des données circulant dans les flux de données sémantiques pour considérer non pas une succession de triplets indépendants mais plutôt une succession de graphes en étoiles, préservant ainsi les liens entre les triplets. En utilisant cette approche, nous avons amélioré significativement la qualité des réponses de quelques algorithmes d’échantillonnage bien connus dans la littérature pour le délestage des flux. L’analyse de la requête continue permet d’optimiser cette solution en repèrant les données non pertinentes pour être délestées les premières. Dans la deuxième contribution, nous proposons un algorithme de détection de motifs fréquents de graphes RDF dans les flux de données RDF, appelé FreGraPaD (Frequent RDF Graph Patterns Detection). C’est un algorithme en une passe, orienté mémoire et peu coûteux. Il utilise deux structures de données principales un vecteur de bits pour construire et identifier le motif de graphe RDF assurant une optimisation de l’espace mémoire et une table de hachage pour le stockage de ces derniers. La troisième contribution de notre thèse consiste en une solution déterministe de réduction de charge des systèmes RSP appelée POL (Pattern Oriented Load-shedding for RDF Stream Processing systems). Elle utilise des opérateurs booléens très peu coûteux, qu’elle applique aux deux motifs binaires construits de la donnée et de la requête continue pour déterminer et éjecter celle qui est non-pertinente. Elle garantit un rappel de 100%, réduit la charge du système et améliore son temps de réponse. Enfin, notre quatrième contribution est un outil de compression en ligne de flux RDF, appelé Patorc (Pattern Oriented Compression for RSP systems). Il se base sur les motifs fréquents présents dans les flux qu’il factorise. C’est une solution de compression sans perte de données dont l’interrogation sans décompression est très envisageable. Les solutions apportées par cette thèse permettent l’extension des systèmes RSP existants en leur permettant le passage à l’échelle dans un contexte de Bigdata. Elles leur permettent ainsi de manipuler un ou plusieurs flux arrivant à différentes vitesses, sans perdre de leur qualité de réponse et tout en garantissant leur disponibilité au-delà même de leurs limites physiques. Les résultats des expérimentations menées montrent que l’extension des systèmes existants par nos solutions améliore leurs performances. Elles illustrent la diminution considérable de leur temps de réponse, l’augmentation de leur seuil de débit de traitement en entrée tout en optimisant l’utilisation de leurs ressources systèmes
Internet is an infinite source of data coming from sources such as social networks or sensors (home automation, smart city, autonomous vehicle, etc.). These heterogeneous and increasingly large data can be managed through semantic web technologies, which propose to homogenize, link these data and reason above them, and data flow management systems, which mainly address the problems related to volume, volatility and continuous querying. The alliance of these two disciplines has seen the growth of semantic data stream management systems also called RSP (RDF Stream Processing Systems). The objective of this thesis is to allow these systems, via new approaches and "low cost" algorithms, to remain operational, even more efficient, even for large input data volumes and/or with limited system resources.To reach this goal, our thesis is mainly focused on the issue of "Processing semantic data streamsin a context of computer systems with limited resources". It directly contributes to answer the following research questions : (i) How to represent semantic data stream ? And (ii) How to deal with input semantic data when their rates and/or volumes exceed the capabilities of the target system ?As first contribution, we propose an analysis of the data in the semantic data streams in order to consider a succession of star graphs instead of just a success of andependent triples, thus preserving the links between the triples. By using this approach, we significantly impoved the quality of responses of some well known sampling algoithms for load-shedding. The analysis of the continuous query allows the optimisation of this solution by selection the irrelevant data to be load-shedded first. In the second contribution, we propose an algorithm for detecting frequent RDF graph patterns in semantic data streams.We called it FreGraPaD for Frequent RDF Graph Patterns Detection. It is a one pass algorithm, memory oriented and "low-cost". It uses two main data structures : A bit-vector to build and identify the RDF graph pattern, providing thus memory space optimization ; and a hash-table for storing the patterns.The third contribution of our thesis consists of a deterministic load-shedding solution for RSP systems, called POL (Pattern Oriented Load-shedding for RDF Stream Processing systems). It uses very low-cost boolean operators, that we apply on the built binary patterns of the data and the continuous query inorder to determine which data is not relevant to be ejected upstream of the system. It guarantees a recall of 100%, reduces the system load and improves response time. Finally, in the fourth contribution, we propose Patorc (Pattern Oriented Compression for RSP systems). Patorc is an online compression toolfor RDF streams. It is based on the frequent patterns present in RDF data streams that factorizes. It is a data lossless compression solution whith very possible querying without any need to decompression.This thesis provides solutions that allow the extension of existing RSP systems and makes them able to scale in a bigdata context. Thus, these solutions allow the RSP systems to deal with one or more semantic data streams arriving at different speeds, without loosing their response quality while ensuring their availability, even beyond their physical limitations. The conducted experiments, supported by the obtained results show that the extension of existing systems with the new solutions improves their performance. They illustrate the considerable decrease in their engine’s response time, increasing their processing rate threshold while optimizing the use of their system resources

Gli stili APA, Harvard, Vancouver, ISO e altri

32

Azami, Ikram El. "Ingéniérie des Systèmes d'Information Coopératifs, Application aux Systèmes d'Information Hospitaliers". Thesis, Valenciennes, 2012. http://www.theses.fr/2012VALE0013.

Testo completo

Abstract (sommario):

Dans cette thèse, nous traitons les systèmes d’information hospitaliers (SIH), nous analysons leurs problématiques de conception, d’interopérabilité et de communication, dans l’objectif de contribuer à la conception d’un SIH canonique, coopératif, et communicant, ainsi de modéliser les échanges entre ses composants et également avec les autres systèmes impliqués dans la prise en charge du patient dans un réseau de soin. Nous proposons une structure et un modèle de conception d’un SIH canonique en se basant sur trois concepts principaux responsables de la production de l’information médicale, à savoir, le cas pathologique, le Poste de Production de l’Information Médicale (PPIM) et l’activité médicale elle même. Cette dernière, étant modélisée sur la notion d’arbre, permettra une meilleure structuration du processus de soin.Autant, dans l’optique d'assurer la continuité de soins, nous fournissons un modèle d’échange de données médicales à base du standard XML. Ce modèle consiste en un ensemble de données pertinentes organisées autours de cinq catégories : les données du patient, les données sur les antécédents du patient, les données de l’activité médicale, les données des prescriptions médicales et les données sur les documents médicaux (images, compte rendu…).Enfin, nous décrivons une solution d’intégration des systèmes d’information hospitaliers. La solution est inspirée de l’ingénierie des systèmes d’information coopératifs et consiste en une architecture de médiation structurée en trois niveaux : le niveau système d’information, le niveau médiation, et le niveau utilisateur. L’architecture propose une organisation modulaire des systèmes d'information hospitaliers et contribue à satisfaire l’intégration des données, des fonctions et du workflow de l’information médicale
In this thesis, we deal with hospital information systems (HIS), we analyze their design issues, interoperability and communication, with the aim of contributing to the design of a canonical, cooperative, and communicative HIS, and model the exchanges between its components and also with other systems involved in the management of patient in a healthcare network.We propose a structure and a conceptual model of a canonical HIS based on three main concepts involved in the production of healthcare data, namely, the pathological case, the Production Post of Healthcare Data (PPHD) and medical activity itself. The latter, being modeled as a tree, will allow better structuring of the care process.However, in view of ensuring continuity of care, we provide an XML-based model for exchanging medical data. This model consists of a set of relevant data organized around five categories: patient data, data on patient history, data of medical activity, data of medical prescriptions and medical records data (images, reporting ...).Finally, we describe a solution for integrating hospital information systems. The solution is inspired by the engineering of cooperatives information systems and consists of mediation-based architecture, structured into three levels: the level of information systems, the level of mediation, and the user level. The architecture offers a modular organization of hospital information systems and helps to insure data, function and workflow integration

Gli stili APA, Harvard, Vancouver, ISO e altri

33

Cerqueus, Thomas. "Contributions au problème d’hétérogénéité sémantique dans les systèmes pair-à-pair : application à la recherche d’information". Nantes, 2012. http://archive.bu.univ-nantes.fr/pollux/show.action?id=c40274d8-21a2-4f4a-9892-1367fd993b9c.

Testo completo

Abstract (sommario):

Nous considérons des systèmes pair-à-pair (P2P) pour le partage de données dans lesquels chaque pair est libre de choisir l’ontologie qui correspond le mieux à ses besoins pour représenter ses données. Nous parlons alors d’hétérogénéité sémantique. Cette situation est un frein important à l’interopérabilité car les requêtes émises par les pairs peuvent être incomprises par d’autres. Dans un premier temps nous nous focalisons sur la notion d’hétérogénéité sémantique. Nous définissons un ensemble de mesures permettant de caractériser finement l’hétérogénéité d’un système suivant différentes facettes. Dans un deuxième temps nous définissons deux protocoles. Le premier, appelé CorDis, permet de réduire l’hétérogénéité sémantique liée aux disparités entre pairs. Il dissémine des correspondances dans le système afin que les pairs apprennent de nouvelles correspondances. Le second protocole, appelé GoOD-TA, permet de réduire l’hétérogénéité sémantique d’un système liée à son organisation. L’objectif est d’organiser le système de sorte que les pairs proches sémantiquement soient proches dans le système. Ainsi deux pairs deviennent voisins s’ils utilisent la même ontologie ou s’il existe de nombreuses correspondances entre leurs ontologies respectives. Enfin, dans un trois temps, nous proposons l’algorithme DiQuESH pour le routage et le traitement de requêtes top-k dans les systèmes P2P sémantiquement hétérogènes. Cet algorithme permet à un pair d’obtenir les k documents les plus pertinents de son voisinage. Nous montrons expérimentalement que les protocoles CorDis et GoOD-TA améliorent les résultats obtenus par DiQuESH
We consider peer-to-peer (P2P) data sharing systems in which each peer is free to choose the ontology that best fit its needs to represent its data. This is what we call semantic heterogeneity. This situation prevents from perfect interoperability because queries issued by peers may be misunderstood by other peers. First we focus on the notion of semantic heterogeneity because it seems to us that it is a complex notion. We define several measures allowing to precisely characterize semantic heterogeneity of a P2P system according to different facets. Second we define two protocols. The first one, called CorDis, allows to reduce semantic heterogeneity related to the disparities between peers. It disseminates correspondences in the system so that peers learn new correspondences. The second protocol, called GoOD-TA, allows to reduce semantic heterogeneity related to the topology of a system. The goal is to organize it in way that semantically close peers are close in the system. Thus two peers are neighbours if they use the same ontology, or if numerous correspondences exist between their respective ontologies. Third we propose an algorithm called DiQuESH for the routing and the treatment of top-k queries in semantically heterogeneous P2P systems. This algorithm allows a peer to retrieve the k most relevant documents from its neighbourhood. We experimentally show that CorDis and GoOD-TA improve results obtained by DiQuESH

Gli stili APA, Harvard, Vancouver, ISO e altri

34

Panetto, Hervé. "Meta-modèles et modèles pour l'intégration et l'interopérabilité des applications d'entreprises de production". Habilitation à diriger des recherches, Université Henri Poincaré - Nancy I, 2006. http://tel.archives-ouvertes.fr/tel-00119423.

Testo completo

Abstract (sommario):

L'intégration des systèmes consiste à assembler les différentes parties d'un système tout en assurant la compatibilité de l'assemblage ainsi que le bon fonctionnement du système complet. Depuis les années quatre-vingt-dix, l'intégration des systèmes d'entreprise a fait l'objet d'une attention croissante ; elle est ainsi devenue un thème de recherche développé dans plusieurs équipes universitaires et industrielles dans le monde autant que a suscité de nombreux travaux au sein des organisations scientifiques internationales, notamment IFAC et IFIP, et de normalisation, particulièrement IEC, ISO et CEN. Dans ce cadre, l'interopérabilité des systèmes est un moyen pour obtenir l'intégration, fondé sur un couplage faible des parties du système, basé sur la capacité des parties à communiquer entre elles pour accéder et faire appel à leurs fonctionnalités.
Plus récemment, au cours de la dernière décennie, une nouvelle approche d'ingénierie logicielle a été élaborée : l'ingénierie dirigée par les modèles. Dans cette nouvelle approche, les modèles occupent une place de premier plan parmi les artefacts d'ingénierie des systèmes. En effet, ils doivent être suffisamment précis afin de pouvoir être interprétés ou transformés par des outils logiciels, tout en étant mis en correspondance avec les démarches d'ingénierie système. Le rôle central des modèles dans le développement des capacités d'interopérabilité participe notablement à cette qualité, car les processus d'ingénierie de l'interopérabilité des applications sont basés sur des flux de modèles.

Ce mémoire d'Habilitation à Diriger des Recherches est centré sur l'étude des modèles en vue de l'interopérabilité des systèmes, et plus particulièrement des systèmes d'entreprises, centrée sur la représentation des produits. Pour contribuer à la fiabilisation des modèles d'entreprise et de leur interrelations pour l'intégration forte des applications, le projet de recherche proposé dans ce mémoire a pour objectif, dans un contexte d'ingénierie système appliqué aux systèmes de systèmes, de définir, d'étendre et de formaliser les processus de modélisation des systèmes d'entreprise en tenant compte des connaissances, généralement non explicites, des acteurs de ces systèmes. Cette preuve de concept relatif à la formalisation de la connaissance des modèles se base sur la définition d'ontologies, ainsi que la mise en correspondance, la transformation et l'échange de modèles, permettant l'intégration des applications d'entreprise et assurant ainsi des flux d'informations cohérents entre tous les acteurs. Ils nécessitent ainsi de rendre explicite la connaissance tacite des modélisateurs (et opérateurs) sur les processus (et donc les modèles) dont ils sont responsables ou auteurs.

Gli stili APA, Harvard, Vancouver, ISO e altri

35

Labéjof, Jonathan. "R-*, Réflexion au Service de l'Évolution des Systèmes de Systèmes". Phd thesis, Université des Sciences et Technologie de Lille - Lille I, 2012. http://tel.archives-ouvertes.fr/tel-00768568.

Testo completo

Abstract (sommario):

Dans un monde de plus en plus connecté, le besoin d'interconnecter des systèmes hétérogènes apparait de plus en plus présent. Les Systèmes de Systèmes (SoS) sont une approche de supervision et de contrôle global où les systèmes constituants sont caractérisés comme des sous-systèmes du SoS. Certains de ces sous-systèmes peuvent être sujets à un environnement dynamique leur demandant d'évoluer pour répondre à de nouvelles exigences, voire de s'adapter s'ils doivent répondre à un besoin de disponibilité. La principale difficulté dans la gestion des évolutions possibles est qu'elles peuvent impacter plusieurs sous-systèmes connectés, et par extension, une vision globale comme celle proposée par un système de systèmes. Ainsi, les problèmes d'évolution et d'adaptation d'un SoS se posent. Dans un cadre d'ingénierie logicielle, cette thèse propose l'approche R-* qui soutient l'hypothèse que plus un système est Réflexif, et plus il devient capable de s'adapter, et donc d'évoluer. Trois contributions majeures et un cas d'utilisation évalu ́e sont proposés pour justifier l'intérêt de R-*. R-DDS et R-MOM ajoutent la capacité de réflexivité dans des sous-systèmes de communication asynchrones, et R-EMS ajoute la capacité de réflexivité sur la vision globale d'un SoS, incluant ses sous-syst'emes et son environnement. R-DDS ajoute la réflexivité à l'intergiciel de Service de Distribution de Données dédié aux domaines du temps-réel et de l'embarqué. R-MOM remonte en abstraction pour proposer la réflexivité au niveau des fonctionalités d'un intergiciel asynchrone. R-EMS est un système de gestion d'environnement réflexif en support de l'utilisation d'un SoS. Finalement, le cas d'utilisation est une implémentation d'un sous-modèle du système de systèmes TACTICOS de THALES, qui servira également d'environnement d'évaluation.

Gli stili APA, Harvard, Vancouver, ISO e altri

36

Tursi, Angela. "Ontology-based approach for product-driven interoperability of enterprise production systems". Thesis, Nancy 1, 2009. http://www.theses.fr/2009NAN10086/document.

Testo completo

Abstract (sommario):

L'interopérabilité des applications est devenue le leitmotiv des développeurs et concepteurs en ingénierie système. La plupart des approches pour l'interopérabilité existant dans l'entreprise ont pour objectif principal l'ajustement et l'adaptation des types et structures de données nécessaire à la mise en œuvre de collaboration entre entreprises. Dans le domaine des entreprises manufacturières, le produit est une composante centrale. Des travaux scientifiques proposent des solutions pour la prise en compte des systèmes d'information issus des produits, tout au long de leur cycle de vie. Mais ces informations sont souvent non corrélées. La gestion des données de produit (PDM) est couramment mise en œuvre pour gérer toute l'information relative aux produits durant tout leur cycle de vie. Cependant, ces modèles sont généralement des "îlots" indépendants ne tenant pas compte de la problématique d'interopérabilité des applications supportant ces modèles. L'objectif de cette thèse est d'étudier cette problématique d'interopérabilité appliquée aux applications utilisées dans l'entreprise manufacturière et de définir un modèle ontologique de la connaissance des entreprises relatives aux produits qu'elles fabriquent, sur la base de leurs données techniques. Le résultat de ce travail de recherche concerne la formalisation d'une méthodologie d'identification des informations de gestion techniques des produits, sous la forme d'une ontologie, pour l'interopérabilité des applications d'entreprises manufacturières, sur la base des standards existants tels que l'ISO 10303 et l'IEC 62264
In recent years, the enterprise applications interoperability has become the leitmotiv of developers and designers in systems engineering. Most approaches to interoperability in the company have the primary objective of adjustment and adaptation of types and data structures necessary for the implementation of collaboration between companies. In the field of manufacturing, the product is a central component. Scientific works propose solutions taking into account information systems derived from products technical data throughout their life cycle. But this information is often uncorrelated. The management of product data (PDM) is commonly implemented to manage all information concerning products throughout their life cycle. The modelling of management and manufacturing processes is widely applied to both physical products and services. However, these models are generally independent “islands” ignoring the problem of interoperability between applications that support these models. The objective of this thesis is to study the problem of interoperability applied to applications used in the manufacturing environment and to define a model of the ontological knowledge of enterprises related to the products they manufacture, based on technical data, ensuring the interoperability of enterprise systems. The outcome of this research concerns the formalization of a methodology for identifying a product-centric information system in the form of an ontology, for the interoperability of applications in manufacturing companies, based on existing standard such as ISO 10303 and IEC 62264

Gli stili APA, Harvard, Vancouver, ISO e altri

37

Bergougnoux, Quentin. "Co-design et implémentation d’un noyau minimal orienté par sa preuve, et évolution vers les architectures multi-coeur". Thesis, Lille 1, 2019. http://www.theses.fr/2019LIL1I029/document.

Testo completo

Abstract (sommario):

Avec la croissance majeure de l’Internet des Objets et du Cloud Computing, la sécurité dans ces systèmes est devenue un problème majeur. Plusieurs attaques ont eu lieu dans les dernières années, mettant en avant la nécessité de garanties de sécurité fortes sur ces systèmes. La plupart du temps, une vulnérabilité dans le noyau ou un de ses modules est suffisante pour compromettre l’intégralité du système. Établir et prouver des propriétés de sécurité par le biais d’assistants de preuve semble être un grand pas en avant vers l’apport de garanties de sécurité. Cela repose sur l’utilisation de modèles mathématiques dans le but de raisonner sur leur comportement, et d’assurer que ce dernier reste correct. Cependant, en raison de la base de code importante des logiciels s’exécutant dans ces systèmes, plus particulièrement le noyau, cela n’est pas une tâche aisée. La compréhension du fonctionnement interne de ces noyaux, et l’écriture de la preuve associée à une quelconque propriété de sécurité, est de plus en plus difficile à mesure que le noyau grandit en taille. Dans cette thèse, je propose une nouvelle approche de conception de noyau, le proto-noyau. En réduisant les fonctionnalités offertes par le noyau jusqu’à leur plus minimal ensemble, ce modèle, en plus de réduire au maximum la surface d’attaque, réduit le coût de preuve au maximum. Il permet également à un vaste ensemble de systèmes d’être construits par-dessus, considérant que la minimalité des fonctionnalités comprises dans le noyau oblige les fonctionnalités restantes à être implémentées en espace utilisateur. Je propose également dans cette thèse une implémentation complète de ce noyau, sous la forme du proto-noyau Pip. En ne fournissant que les appels systèmes les plus minimaux et indispensables, l’adaptation du noyau à des usages concrets et la faisabilité de la preuve sont assurées. Afin de réduire le coût de transition modèlevers-binaire, la majorité du noyau est écrite directement en Gallina, le langage de l’assistant de preuve Coq, et est automatiquement convertie en code C compilable pendant la phase de compilation. Pip ne repose alors que sur une fine couche d’abstraction matérielle écrite dans des langages de bas niveau, qui ne fournit que les primitives que le modèle requiert, telles que la configuration du matériel. De plus, étant donné que l’Internet des Objets et le Cloud Computing nécessitent aujourd’hui ces architectures, je propose plusieurs extensions au modèle de Pip afin de supporter le matériel multi-cœur. Soutenus par des implémentations, ces modèles permettent d’apporter le proto-noyau Pip dans les architectures multi-coeur, apportant ainsi des garanties de sécurité fortes dans ces environnement. Enfin, je valide mon approche et son implémentation par le biais d’évaluations de performances et d’une preuve de concept de portage de noyau Linux, démontrant ainsi la flexibilité du proto-noyau Pip dans des environnements réels
Due to the major growth of the Internet of Things and Cloud Computing worlds, security in those systems has become a major issue. Many exploits and attacks happened in the last few years, highlighting the need of strong security guarantees on those systems. Most of the times, a vulnerability in the kernel or one of its modules is enough to compromise the whole system. Etablishing and proving security properties through proof assistants seems to be a huge step towards bringing security guarantees. This relies on using mathematical models in order to reason on their behaviour, and prove the latter remains correct. Still, due to the huge and complex code base of the software running on those systems, especially the kernel, this is a tedious task. Understanding the internals of those kernels, and writing an associated proof on some security property, is more and more difficult as the kernel grows in size. In this thesis, I propose a new approach of kernel design, the proto-kernel. By reducing the features provided by the kernel to their most minimal subset, this model, in addition to lowering the attack surface, reduces the cost of the proof effort. It also allows a wide range of systems to be built on top of it, as the minimality of the features embedded into the kernel causes the remaining features to be built at the userland level. I also provide in this thesis a concrete implementation of this model, the Pip proto-kernel. By providing only the most minimal and mandatory system calls, both the usability of the kernel and the feasibility of the proof are ensured. In order to reduce the model-to-binary transition effort, most of the kernel is written directly in Gallina, the language of the Coq Proof Assistant, and is automatically converted to compilable C code during compilation phase. Pip only relies on a thin hardware abstraction layer written in low-level languages, which provides the operations the model requires, such as modifying the hardware configuration. Moreover, as Internet of Things and Cloud Computing use cases would require, I propose some extensions of Pip’s model, in order to support multicore hardware. Backed up by real implementations, those models bring the Pip proto-kernel to multicore architectures, bringing strong security guarantees in those modern environments. Finally, I validate my approach and its implementation through benchmarks and a Linux kernel port proof-of-concept, displaying the flexibility of the Pip proto-kernel in real world environments

Gli stili APA, Harvard, Vancouver, ISO e altri

38

Rouvoy, Romain. "Une démarche à granularité extrêmement fine pour la construction de canevas intergiciels hautement adaptables : applications aux services de transactions". Lille 1, 2006. https://ori-nuxeo.univ-lille1.fr/nuxeo/site/esupversions/7959a934-a6e5-48b2-866f-2bbc36e3159b.

Testo completo

Abstract (sommario):

Cette thèse adresse la problématique de la construction des intergiciels hautement adaptables. Ces intergiciels se caractérisent par une grande diversité des fonctionnalités fournies. Dans le domaine du transactionnel, cette diversité concerne non seulement les modèles de transactions, les protocoles de contrôle de concurrence et de reprise après défaillance, mais aussi les normes et les standards d'intégration. Notre proposition consiste à définir un canevas intergiciel capitalisant la diversité du domaine transactionnel, et permettant de construire des services de transactions hautement adaptables. Ce type de services requiert la mise en place d'une démarche de construction à granularité extrêmement fine afin de pouvoir adapter les nombreuses caractéristiques de l'intergiciel. Nous proposons donc de compléter l'approche issue des exogiciels avec quatre nouveaux éléments. Ainsi, nous définissons le modèle de programmation FracIet à base d'annotations pour favoriser la programmation des abstractions fonctionnelles de l'intergiciel. Nous proposons ensuite un langage de description et de vérification de motif d'architecture pour fiabiliser la modélisation des abstractions architecturales. Ces deux premiers éléments servent à la conception d'un canevas intergiciel à base de composants utilisant les motifs de conception comme structure architecturale extensible. Enfin, nous décrivons les configurations possibles en utilisant différents modèles de haut niveau dédiés aux caractéristiques de l'intergiciel. Nous illustrons ces concepts en présentant GoTM, un caneva intergiciel à composants pour la construction de services de transactions hautement adaptables. Notre approche est validée au travers de trois expériences originales. Tout d'abord, nous proposons de faciliter l'intégration des services de transactions dans les plates-formes intergicielles par la définition de politiques de démarcation transactionnelle indépendantes de la plate-forme et du type de service intégré. Ensuite, nous définissons un service de transactions composant plusieurs personnalités simultanément pour faciliter l'interopérabilité transactionnelle d'applications hétérogènes. Enfin, nous sommes en mesure de sélectionner différents protocoles de validation à deux phases pour optimiser le temps d'exécution des transactions face aux changements des condition d'exécution de l'application

Gli stili APA, Harvard, Vancouver, ISO e altri

39

Belaud, Jean-Pierre. "Architecture et technologies des systèmes logiciels ouverts : CAPE-OPEN, un standard pour l'interopérabilité et l'intégration des composants logiciels de l'ingénierie des procédés". Toulouse, INPT, 2002. http://www.theses.fr/2002INPT026G.

Testo completo

Abstract (sommario):

Les progiciels de l'ingénierie des procédés sont spécifiques à chaque éditeur. Ceci conduit à une hétérogénéité des solutions qui limite l'intégration des savoir-faire tiers. Le syst-me cape-open (CO) propose des interfaces de programmation standartisées. Il définit une architecture ouverte permettant l'interopérabilité et l'intégration des composants logiciels pour la simultation des procédés. Ce système est caractérisé par une architecture technique des spécifications d'interface et des spécifications d'implémentation. L'architecture technique repose sur une approche orientée-objet/composants, une architecture distribuée web, la technologie middleware et UML. Les spécifications d'interface documentent un modèle conceptuel et les spécifications d'implémentation décrivent ce modèle pour les plates-formes COM et CORBA. Les spécifications Opération Unitaire, Parmètre et Contexte de Simulation sont détaillées. Des composants logiciels compatibles CO sont développés dont un analyseur de graphes de procédés et un serveur de méthodes numériques. CO est du domaine public et est régi par un consortium international, CO-LaN, qui regroupe les différents acteurs : industiels, éditeurs et universitaires.

Gli stili APA, Harvard, Vancouver, ISO e altri

40

Rezgui, Abir. "Interopérabilité de modèles dans le cycle de conception des systèmes électromagnétiques via des supports complémentaires : VHDL-AMS et composants logiciels ICAr". Phd thesis, Université de Grenoble, 2012. http://tel.archives-ouvertes.fr/tel-00858315.

Testo completo

Abstract (sommario):

Cette thèse aborde les formalismes pour la modélisation multi-physique en support au cycle en V deconception. Ce travail a été réalisé dans le cadre du projet ANR-MoCoSyMec, selon la méthodologie duprototypage virtuel fonctionnel (PVF) et illustré sur des systèmes électromagnétiques.Nous nous sommes principalement intéressés au langage VHDL-AMS, en tant que support aux différentsniveaux de modélisation apparaissant dans le cycle en V de conception. Cela nous a conduits à traiter laportabilité et l'interopérabilité en VHDL-AMS de diverses méthodes et outils de modélisation. Nous avonsproposé et validé, via le formalisme des composants logiciels ICAr, des solutions aux limites de l'utilisation deVHDL-AMS pour modéliser certains phénomènes physiques reposants sur des calculs numériques.Nous avons étendu la norme ICAr pour supporter des modèles dynamiques décrits par des équationsdifférentielles algébriques (DAE) ; et pour des besoins de co-simulation, nous pouvons également y associer unsolveur. Ces développements sont désormais capitalisés dans le framework CADES.Enfin, nous avons proposé une architecture pour le portage de modèles d'un formalisme à un autre. Elle a étédéfinie et mise en oeuvre plus particulièrement pour des modèles magnétiques réluctants (Reluctool) et desMEMS magnétiques (MacMMems) vers le VHDL-AMS.Ces formalismes et méthodologies sont mis en oeuvre autour du PVF d'un contacteur électromagnétique.

Gli stili APA, Harvard, Vancouver, ISO e altri

41

Viard, Louis. "Méthodes et outils pour la programmation des systèmes cyber-physiques". Electronic Thesis or Diss., Université de Lorraine, 2021. http://www.theses.fr/2021LORR0105.

Testo completo

Abstract (sommario):

La conception de systèmes cyber-physiques est une discipline émergente à l'interface de nombreux domaines d'ingénierie. Ces systèmes se caractérisent notamment par une identité double, liant le monde des contrôleurs, discret, à celui du matériel, continu. Les errements d'un contrôleur, qu'ils soient dus à un programme erroné ou à la manifestation d'un aléa de l'environnement, sont susceptibles de produire des conséquences désastreuses. Une attention particulière doit donc être apportée à leur programmation. Le travail présenté dans cet ouvrage est une réponse à ce défi. Nous proposons un langage dédié à la programmation des systèmes cyber-physiques, Sophrosyne, ainsi qu'une méthode formelle de vérification des missions résultantes. Le langage repose sur des structures de supervision, permettant au système d'adapter son comportement selon la survenance d'aléas. Il présente de plus un volet de modélisation continue du système au moyen d'équations différentielles, duquel dérive la vérification formelle des missions exprimée en logique dynamique différentielle. Divers outils ont été développés autour de Sophrosyne pour assurer la planification, la compilation, l'analyse, et l'exécution de missions. Ils constituent une chaîne logicielle complète allant d'une interface graphique assistant la conception de mission jusqu'à son exécution sur le système réel. Ces outils ont été mis en œuvre sur des projets d'inspections aériennes d'infrastructures par drone. Les travaux présentés sont illustrés par ces applications drones
Building cyber-physical systems is an up-and-coming discipline which involves many engineering domains. Cyber-physical systems have a controller monitoring their physical behaviour, resulting in intertwined discrete and continuous evolution. Faulty programs or environmental hazards might lead to unwanted control and disastrous consequences. Safe operation of cyber-physical systems requires to pay dedicated attention to their programming. Our work attempts to provide a solution to this challenge. We present a domain specific language for programming cyber-physical systems, Sophrosyne, as well as a formal method to verify the correction of the resulting missions. The language is based on monitoring control structures, which provide reactive behaviours to the system. It furthermore includes continuous modelling of the system with differential equations to enable verification of missions using differential dynamic logic. Various softwares have been built to provide Sophrosyne with mission planification, compilation, analysis, and execution. Together they form a complete toolchain from a graphical user interface supporting the definition of a mission to its execution on the real system. These tools have been used to define aerial inspections of infrastructure with unmanned aircraft. We demonstrate our contribution on such applications

Gli stili APA, Harvard, Vancouver, ISO e altri

42

Régis-Gianas, Yann. "Des types aux assertions logiques : preuve automatique ou assistée de propriétés sur les programmes fonctionnels". Paris 7, 2007. http://www.theses.fr/2007PA077155.

Testo completo

Abstract (sommario):

Cette thèse étudie deux approches pour augmenter la sûreté de fonctionnement des programmes informatiques par analyse statique. La première approche est l'utilisation du typage qui permet de prouver automatiquement qu'un programme s'évalue sans échouer. Le langage fonctionnel ML possède un système de type très riche et un algorithme effectuant une synthèse automatique des types. On s'intéresse à son adaptation aux types algébriques généralisés (GADT). Dans ce cadre, le calcul efficace d'un type plus général est impossible. On propose une stratification du langage qui maintient les caractéristiques habituelles sur le fragment ML et qui isole le traitement des GADT en explicitant leur utilisation. Le langage obtenu, MLGX, nécessite des annotations de type qui alourdissent les programmes. Une seconde strate, MLGI, offre au programmeur un mécanisme de synthèse locale, prédictible et efficace bien qu'incomplet, de la plupart de ces annotations. La première partie s'achève avec une démonstration de l'expressivité des GADT pour coder les invariants des automates à pile utilisés par l'analyse syntaxique LR. La seconde approche augmente le langage par des assertions logiques permettant d'exprimer des spécifications de complexité arbitraire. On vérifie la conformité de la sémantique du programme vis-à-vis de ces spécifications à l'aide d'une technique appelée logique de Hoare et d'outils semi-automatique de preuves mathématiques sur ordinateur. Les choix de conception du système permettent de traiter les fonctions de première classe. Ils sont dirigés par une implantation qui trouve une illustration dans la certification d'un module d'arbres dénotant des ensembles finis
This work studies two approaches to improve the safety of computer programs using static analysis. The first one is typing which guarantees that the evaluation of program cannot fail. The functional language ML has a very rich type system and also an algorithm that infers automatically the types. We focus on its adaptation to generalized algebraic datatypes (GADTs). In this setting, efficient computation of a most general type is impossible. We propose a stratification of the language that retains the usual caracteristics of the ML fragment and make explicit the use of GADTs. The resulting language, MLGX, entails a burden on the programmer who must annotate its programs too much. A second stratum, MLGI, offers a mecanism to infer locally, in a predictable and efficient but incomplete way most of the type annotations. The first part ends up on an illustration of thé expressiveness of GADTs to encode the invariants of pushdown automata used In LR parsing. The second approach augments the language with logic assertions that enable arbitrarily compiex specifications to be expressed. We check the compliance of the program semantics with respect to these specifications thanks to a method called Hoare logic and thanks to semi-automatic computer-based proofs. The design choices permit to handle first-class functions. They are directed by an implementation which is illustrated by the certifiction of a module of trees that denote finite sets

Gli stili APA, Harvard, Vancouver, ISO e altri

43

Motie, Yassine. "Interopérabilité entre dispositifs hétérogènes en environnement ouvert pour la mise en oeuvre de co-simulation". Thesis, Toulouse 3, 2019. http://www.theses.fr/2019TOU30102.

Testo completo

Abstract (sommario):

Le grand nombre de fonctionnalités d'appareils électroniques qu'on utilise quotidiennement entraîne le passage d'une vision centrée sur des anciennes machines multifonctions vers des appareils variées en interaction distribués et éparpillés dans l'environnement. Sachant qu'un système est un ensemble intégré d'éléments (produits, personnels, processus) connectés et reliés entre eux, en vue de satisfaire, dans un environnement donné, un ou plusieurs objectifs définis et ayant des caractéristiques comme les composants qui le constituent, les relations entre ces composants, son environnement, les contraintes qu'il subit, les évolutions au cours du temps. La combinaison de ces derniers nous conduit à qualifier certains systèmes comme étant complexes dû à l'hétérogénéité des composants les constituant, à leurs évolution à diverses échelles de temps et à leurs répartition géographique intégrant des systèmes numériques, physiques et/ou des opérateurs humains dans la boucle. La difficulté d'avoir une bonne vision du système quand il est complexe (dispositifs réels et d'autres simulés) et la probabilité d'erreur de conception importante nous amène à réfléchir sur la possibilité de spécifier le produit et vérifier la conception à l'aide d'un prototype virtuel, on parle de simulation. Quand un système complexe nécessite l'emploi de différents composants spécifiés par différents concepteurs travaillant sur des domaines différents, ceci augmente fortement le nombre de prototypes virtuels. Ces différents composants ont malheureusement tendance à demeurer trop indépendants les uns des autres empêchant ainsi à la fois les différents concepteurs de collaborer et leurs systèmes d'être interconnectés en vue de remplir une ou plusieurs tâches qui ne pourraient pas être accomplies par l'un de ces éléments seulement. Le besoin de communication et de coopération s'impose. Cela doit tenir compte des différents acteurs et les coordonner dans leurs interactions au sein de ce système complexe. Or les avancées en simulation dans chacun des domaines sont considérables, chacun disposant de ses propres logiciels. Des solutions d'interopérabilités sont donc nécessaires pour la mise en œuvre d'une co-simulation encourageant le dialogue entre les disciplines et réduisant les erreurs, le coût et le temps de développement. Dans notre thèse nous participons à la conception d'un système de co-simulation qui intègre différents outils de simulation-métiers basés sur la modélisation du comportement de dispositifs comme la simulation énergétique et la simulation d'usure de matériaux de construction au sein de la même plateforme. Après la prise en compte des notions d'architecture, de communication (entre les simulateurs ou avec les utilisateurs) et de visualisation pour définir les modèles d'architecture. Nous analysons l'architecture gérant l'interopérabilité. Nous proposons une approche d'interopérabilité se basant sur la réutilisation et l'échange de composants de calculs. Nous aborderons successivement les problématiques liées aux niveaux structurel et sémantique d'interopérabilité, aux stratégies co-simulation, aux méthodes de conception du modèle de tâches permettant la construction de composants boite noire. Puis nous présenterons la mise en application concrète de notre méthodologie de conception globale et de l'outil de vérification de certaines propriétés de l'architecture, comme la cohérence et la sémantique
The large number of electronic device features we use on a daily basis means a shift from a vision of old multifunction machines to distributed, widely distributed distributed devices in the environment. Knowing that a system is an integrated set of connected and interrelated elements (products, people, processes) in order to satisfy, in a given environment, one or more defined objectives and having characteristics such as the components that constitute it , the relations between these components, its environment, the constraints it undergoes, evolutions over time. The combination of these leads us to qualify some systems as complex due to the heterogeneity of the components constituting them, their evolution at various time scales and their geographical distribution integrating digital systems, physical and / or human operators in the loop. The difficulty of having a good vision of the system when it is complex (real and other simulated devices) and the probability of significant design error leads us to reflect on the ability to specify the product and verify the design using a virtual prototype, we are talking about simulation. When a complex system requires the use of different components specified by different designers working on different domains, this greatly increases the number of virtual prototypes. These different components unfortunately tend to remain too independent of each other thus preventing both the different designers from collaborating and their systems from being interconnected in order to fulfill one or more tasks that could not be accomplished by one of these elements only. The need for communication and cooperation is needed. This must take into account the different actors and coordinate them in their interactions within this complex system. But the advances in simulation in each area are considerable, each with its own software. Interoperability solutions are therefore necessary for the implementation of a co-simulation encouraging dialogue between disciplines and reducing errors, cost and development time. In our thesis we participate in the design of a co-simulation system which integrates different tools of simulation-trades based on the modeling of the behavior of devices like the simulation energetics and the simulation of wear of building materials within the same platform. After taking into account the concepts of architecture, communication (between simulators or with users) and visualization to define architecture models. We analyze the architecture that manages interoperability. We propose an interoperability approach based on the reuse and exchange of computational components. We will successively address the issues related to the interoperability structural and semantic levels, the co-simulation strategies, the design methods of the task model allowing the construction of black box components. Then we will present the concrete implementation of our global design methodology and the verification tool of some properties of the architecture, such as coherence and semantics

Gli stili APA, Harvard, Vancouver, ISO e altri

44

El, Hami Norelislam. "Contribution aux méthodes hybrides d'optimisation heuristique : Distribution et application à l'interopérabilité des systèmes d'information". Phd thesis, INSA de Rouen, 2012. http://tel.archives-ouvertes.fr/tel-00771360.

Testo completo

Abstract (sommario):

Les travaux présentés dans ce mémoire proposent une nouvelle méthode d'optimisation globale dénommée MPSO-SA. Cette méthode hybride est le résultat d'un couplage d'une variante d'algorithme par Essaim de particules nommé MPSO (Particle Swarm Optimization) avec la méthode du recuit simulé nommé SA (Simulted Annealing). Les méthodes stochastiques ont connu une progression considérable pour la résolution de problèmes d'optimisation. Parmi ces méthodes, il y a la méthode Essaim de particules (PSO° qui est développée par [Eberhart et Kennedy (1995)]. Quant à la méthode recuit simulé (SA), elle provient du processus physique qui consiste à ordonner les atomes d'un cristal afin de former une structure cristalline parfaite. Pour illustrer les performances de la méthode MPSO-SA proposée, une comparaison avec MPSO et SA est effectuée sur des fonctions tests connues dans la littérature. La métode MPSO-SA est utilisée pour la résolution des problèmes réels interopérabilité des systèmes d'information, ainsi qu'aux problèmes d'optimisation et de fiabilité des structures mécaniques.

Gli stili APA, Harvard, Vancouver, ISO e altri

45

Grieu, Jérôme. "Analyse et évaluation de techniques de commutation Ethernet pour l'interconnexion des systèmes avioniques". Phd thesis, Toulouse, INPT, 2004. http://oatao.univ-toulouse.fr/7385/1/grieu.pdf.

Testo completo

Abstract (sommario):

Les nouvelles générations d'aéronefs embarquent de plus en plus de systèmes avioniques, pour augmenter à la fois la sécurité et le confort des passagers, tout en maintenant une haute rentabilité pour les compagnies aériennes. Ces nouvelles fonctions entraînent une forte hausse des échanges de données, ce qui nécessite plus de débit et de possibilités d'interconnexion. Les bus classiques de communications avioniques ne peuvent répondre à cette nouvelle demande, ce qui a poussé les constructeurs Airbus et Boeing à installer à bord un réseau de communication utilisant la technologie Ethernet commuté. Le principal apport de cette thèse est le développement d'une méthode de preuve du déterminisme de ce type de réseaux, démonstration fondamentale pour permettre leur certification aéronautique. Cette méthode, utilisant la théorie du Network Calculus, a été retenue par Airbus pour la certification du réseau AFDX de l'A380. Nous proposons également des optimisations de ce réseau (politiques de service des commutateurs, interconnexion des éléments réseau) en vue d'améliorer les résultats de son analyse de déterminisme par la méthode précédente. Enfin, nous proposons une extension de nature stochastique à notre méthode déterministe, qui pourrait dans le cadre d'un futur programme permettre de dimensionner au plus juste les ressources physiques du réseau.

Gli stili APA, Harvard, Vancouver, ISO e altri

46

Kan, Channmeta. "Le rôle du juge dans l'administration de la preuve : étude comparée des grands systèmes dans les différents pays de l'ASEAN". Lyon 3, 2007. https://scd-resnum.univ-lyon3.fr/in/theses/2007_in_kan_c.pdf.

Testo completo

Abstract (sommario):

Pour étudier le rôle du juge dans l'administration de la preuve dans le nouveau Code de procédure civile cambodgien, a été choisie la méthode comparative non seulement avec le droit antérieur à l'entrée en vigueur de ce Code et notamment l'ancien Code de procédure en matière civile de 1965, mais également avec cinq autres pays de l'ASEAN : la Thaïlande, le Vietnam, la Malaisie, Singapour et les Philippines. L'étude des dispositions du nouveau Code seule ne suffit pas à apprécier la valeur inestimable du travail de la Commission métissée khméro-japonaise depuis dix années. Le droit comparé paraît être la seule méthode qui permette de percevoir clairement l'évolution interne et externe de notre droit, de mettre en exergue des lacunes, de trouver des moyens de perfectionnement, de les améliorer en les adaptant aux besoins de la société. Les conflits fonciers deviennent de plus en plus importants, les conflits conjugaux et de voisinage le sont toujours, même s'ils tendent à baisser en raison du renforcement de l'éducation, de la mise en valeur des droits de l'homme par toute sorte de méthode de diffusion et surtout de nouveaux textes de lois. Le traitement du conflit est encore fondé sur la conciliation quelle que soit sa nature. La notion de preuve et de procédés de preuve est assez marginalisée en dehors du procès. Le juge rencontre par ailleurs des difficultés résultant des lacunes des textes écrits. Le peuple cambodgien a attendu avec impatience l'arrivée du nouveau Code comprenant des dispositions claires, courtes et précises. D'après ce nouveau Code, il serait inexact que le juge cambodgien joue un rôle passif dans l'administration de la preuve, mais il serait également erroné de dire que les dispositions sur le rôle du juge dans l'administration de la preuve sont suffisantes, complètes et cohérentes. Il existe plusieurs points à améliorer dans les jours, les mois, les années qui viennent : la charge de la preuve, l'aveu, le serment, l'attestation d'enquête et d'expertise, le pouvoir d'initiative de l'expert. Il est néanmoins important de saluer le travail précieux et soigné de la Commission khméro-japonaise qui est parvenue à aboutir à un code permettant de combler un vide de plus de trente années. Pour parvenir à la réalité et vérité, il est en encore nécessaire d'avoir une meilleure collaboration entre le juge et les parties et entre le juge et les tiers, mais il faut également des dispositions sur l'administration de la preuve plus rigides, plus complètes, plus cohérentes, un statut complet de la déontologie du juge et un pouvoir judiciaire indépendant.

Gli stili APA, Harvard, Vancouver, ISO e altri

47

Singh, Neeraj Kumar. "Fiabilité et sûreté des systèmes informatiques critiques". Thesis, Nancy 1, 2011. http://www.theses.fr/2011NAN10129/document.

Testo completo

Abstract (sommario):

Les systèmes informatiques envahissent notre vie quotidienne et sont devenus des éléments essentiels de chacun de nos instants de vie. La technologie de l'information est un secteur d'activités offrant des opportunités considérables pour l'innovation et cet aspect paraît sans limite. Cependant, des systèmes à logiciel intégré ont donné des résultats décevants. Selon les constats, ils étaient non fiables, parfois dangereux et ne fournissaient pas les résultats attendus. La faiblesse des pratiques de développement constitue la principale raison des échecs de ces systèmes. Ceci est dû à la complexité des logiciels modernes et au manque de connaissances adéquates et propres. Le développement logiciel fournit un cadre contribuant à simplifier la conception de systèmes complexes, afin d'en obtenir une meilleure compréhension et d'assurer une très grande qualité à un coût moindre. Dans les domaines de l'automatique, de la surveillance médicale, de l'avionique..., les systèmes embarqués hautement critiques sont candidats aux erreurs pouvant conduire à des conséquences graves en cas d'échecs. La thèse vise à résoudre ce problème, en fournissant un ensemble de techniques, d'outils et un cadre pour développer des systèmes hautement critiques, en utilisant des techniques formelles à partir de l'analyse des exigences jusqu'à la production automatique de code source, en considérant plusieurs niveaux intermédiaires. Elle est structurée en deux parties: d'une part des techniques et des outils et d'autre part des études de cas. La partie concernant des techniques et des outils présente une structure intégrant un animateur de modèles en temps-réel, un cadre de correction de modèles et le concept de charte de raffinement, un cadre de modélisation en vue de la certification, un modèle du coeur pour la modélisation en boucle fermée et des outils de générations automatiques de code. Ces cadres et outils sont utilisés pour développer les systèmes critiques à partir de l'analyse des exigences jusqu'à la production du code, en vérifiant et en validant les étapes intermédiaires en vue de fournir un modèle formel correct satisfaisant les propriétés souhaitées attendues au niveau le plus concret. L'introduction de nouveaux outils concourt à améliorer la vérification des propriétés souhaitées qui ne sont pas apparentes aux étapes initiales du développement du système. Nous évaluons les propositions faites au travers de cas d'études du domaine médical et du domaine des transports. De plus, le travail de cette thèse a étudié la représentation formelle des protocoles médicaux, afin d'améliorer les protocoles existants. Nous avons complètement formalisé un protocole réel d'interprétation des ECG, en vue d'analyser si la formalisation était conforme à certaines propriétés relevant du protocole. Le processus de vérification formelle a mis en évidence des anomalies dans les protocoles existants. Nous avons aussi découvert une structure hiérarchique pour une interprétation efficace permettant de découvrir un ensemble de conditions qui peuvent être utiles pour diagnostiquer des maladies particulières à un stade précoce. L'objectif principal du formalisme développé est de tester la correction et la consistance du protocole médical
Software systems are pervasive in all walks of our life and have become an essential part of our daily life. Information technology is one major area, which provides powerful and adaptable opportunities for innovation, and it seems boundless. However, systems developed using computer-based logic have produced disappointing results. According to stakeholders, they are unreliable, at times dangerous, and fail to provide the desired outcomes. Most significant reasons of system failures are the poor development practices for system development. This is due to the complex nature of modern software and lack of adequate and proper understanding. Software development provides a framework for simplifying the complex system to get a better understanding and to develop the higher fidelity quality systems at lower cost. Highly embedded critical systems, in areas such as automation, medical surveillance, avionics, etc., are susceptible to errors, which can lead to grave consequences in case of failures. This thesis intends to contribute to further the use of formal techniques for the development computing systems with high integrity. Specifically, it addresses that formal methods are not well integrated into established critical systems development processes by defining a new development life-cycle, and a set of associated techniques and tools to develop highly critical systems using formal techniques from requirements analysis to automatic source code generation using several intermediate layers with rigorous safety assessment approach. The approach has been realised using the Event-B formalism. This thesis has mainly two parts: techniques and tools and case studies. The techniques and tools section consists of development life-cycle methodology, a framework for real-time animator, refinement chart, a set of automatic code generation tools and formal logic based heart model for close loop modeling. New development methodology, and a set of associated techniques and tools are used for developing the critical systems from requirements analysis to code implementation, where verification and validation tasks are used as intermediate layers for providing a correct formal model with desired system behavior at the concrete level. Introducing new tools help to verify desired properties, which are hidden at the early stage of the system development. We also critically evaluate the proposed development methodology and developed techniques and tools through case studies in the medical and automotive domains. In addition, the thesis work tries to address the formal representation of medical protocols, which is useful for improving the existing medical protocols. We have fully formalised a real-world medical protocol (ECG interpretation) to analyse whether the formalisation complies with certain medically relevant protocol properties. The formal verification process has discovered a number of anomalies in the existing protocols. We have also discovered a hierarchical structure for the ECG interpretation efficiently that helps to find a set of conditions that can be very helpful to diagnose particular disease at the early stage. The main objective of the developed formalism is to test correctness and consistency of the medical protocol

Gli stili APA, Harvard, Vancouver, ISO e altri

48

Radhouani, Amira. "Méthodes formelles pour l'extraction d'attaques internes des Systèmes d'Information". Thesis, Université Grenoble Alpes (ComUE), 2017. http://www.theses.fr/2017GREAM025/document.

Testo completo

Abstract (sommario):

La sécurité des Systèmes d’Information (SI) constitue un défi majeur car elle conditionne amplement la future exploitation d’un SI. C’est pourquoi l’étude des vulnérabilités d’un SI dès les phases conceptuelles est cruciale. Il s’agit d’étudier la validation de politiques de sécurité, souvent exprimées par des règles de contrôle d’accès, et d’effectuer des vérifications automatisées sur des modèles afin de garantir une certaine confiance dans le SI avant son opérationnalisation. Notre intérêt porte plus particulièrement sur la détection des vulnérabilités pouvant être exploitées par des utilisateurs internes afin de commettre des attaques, appelées attaques internes, en profitant de leur accès légitime au système. Pour ce faire, nous exploitons des spécifications formelles B générées, par la plateforme B4MSecure, à partir de modèles fonctionnels UML et d’une description Secure UML des règles de contrôle d’accès basées sur les rôles. Ces vulnérabilités étant dues à l’évolution dynamique de l’état fonctionnel du système, nous proposons d’étudier l’atteignabilité des états, dits indésirables, donnant lieu à des attaques potentielles, à partir d’un état normal du système. Les techniques proposées constituent une alternative aux techniques de model-checking. En effet, elles mettent en œuvre une recherche symbolique vers l’arrière fondée sur des approches complémentaires : la preuve et la résolution de contraintes. Ce processus de recherche est entièrement automatisé grâce à notre outil GenISIS qui a montré, sur la base d’études de cas disponibles dans la littérature, sa capacité à retrouver des attaques déjà publiées mais aussi des attaques nouvelles
The early detection of potential threats during the modelling phase of a Secure Information System (IS) is required because it favours the design of a robust access control policy and the prevention of malicious behaviours during the system execution. This involves studying the validation of access control rules and performing vulnerabilities automated checks before the IS operationalization. We are particularly interested in detecting vulnerabilities that can be exploited by internal trusted users to commit attacks, called insider attacks, by taking advantage of their legitimate access to the system. To do so, we use formal B specifications which are generated by the B4MSecure platform from UML functional models and a SecureUML modelling of role-based access control rules. Since these vulnerabilities are due to the dynamic evolution of the functional state, we propose to study the reachability of someundesirable states starting from a normal state of the system. The proposed techniques are an alternative to model-checking techniques. Indeed, they implement symbolic backward search algorithm based on complementary approaches: proof and constraint solving. This rich technical background allowed the development of the GenISIS tool which automates our approach and which was successfully experimented on several case studies available in the literature. These experiments showed its capability to extract already published attacks but also new attacks

Gli stili APA, Harvard, Vancouver, ISO e altri

49

Liao, Yongxin. "Annotations sémantiques pour l'intéropérabilité des systèmes dans un environnement PLM". Electronic Thesis or Diss., Université de Lorraine, 2013. http://www.theses.fr/2013LORR0135.

Testo completo

Abstract (sommario):

Dans l'industrie l'approche de gestion du cycle de vie du produit (PLM) a été considérée comme une solution essentielle pour améliorer la compétitivité des produits. Elle vise à fournir une plate-forme commune qui rassemble les différents systèmes de l'entreprise à chaque étape du cycle de vie du produit dans ou à travers les entreprises. Bien que les principaux éditeurs de logiciels fassent des efforts pour créer des outils offrant un ensemble complet et intégré de systèmes, la plupart d' entre eux n'intègrent pas l'ensemble des systèmes. Enfin, ils ne fournissent pas une intégration cohérente de l'ensemble du système d'information. Il en résulte une sorte de « tour de Babel », où chaque application est considérée comme une île au milieu de l'océan de l'information, gérée par de nombreuses parties prenantes dans une entreprise, ou même dans un réseau d'entreprises. L'hétérogénéité des parties prenantes augmente le problème d'interopérabilité. L'objectif de cette thèse est de traiter la question de l'interopérabilité sémantique, en proposant une méthode d'annotation sémantique formelle pour favoriser la compréhension mutuelle de la sémantique de l'information partagée et échangée dans un environnement PLM
In manufacturing enterprises the Product Lifecycle Management (PLM) approach has been considered as an essential solution for improving the product competitive ability. It aims at providing a shared platform that brings together different enterprise systems at each stage of a product life cycle in or across enterprises. Although the main software companies are making efforts to create tools for offering a complete and integrated set of systems, most of them have not implemented all of the systems. Finally, they do not provide a coherent integration of the entire information system. This results in a kind of "tower of Babel", where each application is considered as an island in the middle of the ocean of information, managed by many stakeholders in an enterprise, or even in a network of enterprises. The different peculiarities of those stakeholders are then over increasing the issue of interoperability. The objective of this thesis is to deal with the issue of semantic interoperability, by proposing a formal semantic annotation method to support the mutual understanding of the semantics inside the shared and exchanged information in a PLM environment

Gli stili APA, Harvard, Vancouver, ISO e altri

50

Boudjani, Nadira. "Aide à la construction et l'évaluation des preuves mathématiques déductives par les systèmes d'argumentation". Thesis, Montpellier, 2018. http://www.theses.fr/2018MONTS060/document.

Testo completo

Abstract (sommario):

L'apprentissage des preuves mathématiques déductives est fondamental dans l'enseignement des mathématiques. Pourtant, la dernière enquête TIMSS (Trends in International Mathematics and Science Study) menée par l'IEA ("International Association for the Evaluation of Educational Achievement") en mars 2015, le niveau général des étudiants en mathématiques est en baisse et les étudiants éprouvent de plus en plus de difficultés pour comprendre et écrire les preuves mathématiques déductives.Pour aborder ce problème, plusieurs travaux en didactique des mathématiques utilisent l’apprentissage collaboratif en classe.L'apprentissage collaboratif consiste à regrouper des étudiants pour travailler ensemble dans le but d'atteindre un objectif commun. Il repose sur le débat et l'argumentation. Les étudiants s'engagent dans des discussions pour exprimer leurs points de vue sous forme d'arguments et de contre-arguments dans le but de résoudre un problème posé.L’argumentation utilisée dans ces approches est basée sur des discussions informelles qui permettent aux étudiants d'exprimer publiquement leurs déclarations et de les justifier pour construire des preuves déductives. Ces travaux ont montré que l’argumentation est une méthode efficace pour l’apprentissage des preuves mathématiques : (i) elle améliore la pensée critique et les compétences métacognitives telles que l'auto-surveillance et l'auto-évaluation (ii) augmente la motivation des étudiants par les interactions sociales et (iii) favorise l'apprentissage entre les étudiants. Du point de vuedes enseignants, certaines difficultés surgissent avec ces approches pour l'évaluation des preuves déductives. En particulier, l'évaluation des résultats, qui comprend non seulement la preuve finale mais aussi les étapes intermédiaires, les discussions, les conflits qui peuvent exister entre les étudiants durant le débat. En effet, cette évaluation introduit une charge de travail importante pour les enseignants.Dans cette thèse, nous proposons un système pour la construction et l'évaluation des preuves mathématiques déductives. Ce système a un double objectif : (i) permettre aux étudiants de construire des preuves mathématiques déductives à partir un débat argumentatif structuré (ii) aider les enseignants à évaluer ces preuves et toutes les étapes intermédiaires afin d'identifier les erreurs et les lacunes et de fournir un retour constructif aux étudiants.Le système offre aux étudiants un cadre structuré pour débattre durant la construction de la preuve en utilisant les cadres d'argumentation proposés en intelligente artificielle. Ces cadres d’argumentation sont utilisés aussi dans l’analyse du débat qui servira pour représenter le résultat sous différentes formes afin de faciliter l’évaluation aux enseignants. Dans un second temps, nous avons implanté et validé le système par une étude expérimentale pour évaluer son acceptabilité dans la construction collaborative des preuves déductives par les étudiants et dans l’évaluation de ces preuves par les enseignants
Learning deductive proofs is fundamental for mathematics education. Yet, many students have difficulties to understand and write deductive mathematical proofs which has severe consequences for problem solving as highlighted by several studies. According to the recent study of TIMSS (Trends in International Mathematics and Science Study), the level of students in mathematics is falling. students have difficulties to understand mathematics and more precisely to build and structure mathematical proofs.To tackle this problem, several approaches in mathematical didactics have used a social approach in classrooms where students are engaged in a debate and use argumentation in order to build proofs.The term "argumentation" in this context refers to the use of informal discussions in classrooms to allow students to publicly express claims and justify them to build proofs for a given problem. The underlying hypotheses are that argumentation: (i) enhances critical thinking and meta-cognitive skills such as self monitoring and self assessment; (ii) increases student's motivation by social interactions; and (iii) allows learning among students. From instructors' point of view, some difficulties arise with these approaches for assessment. In fact, the evaluation of outcomes -- that includes not only the final proof but also all intermediary steps and aborted attempts -- introduces an important work overhead.In this thesis, we propose a system for constructing and evaluating deductive mathematical proofs. The system has a twofold objective: (i) allow students to build deductive mathematical proofs using structured argumentative debate; (ii) help the instructors to evaluate these proofs and assess all intermediary steps in order to identify misconceptions and provide a constructive feedback to students. The system provides students with a structured framework to debate during construction of proofs using the proposed argumentation frameworks in artificial intelligence. These argumentation frameworks are also used in the analysis of the debate which will be used to represent the result in different forms in order to facilitate the evaluation to the instructors. The system has been implemented and evaluated experimentally by students in the construction of deductive proofs and instructors in the evaluation of these proofs

Gli stili APA, Harvard, Vancouver, ISO e altri

Tesi sul tema "Interopérabilité des systèmes de preuve"

Cita una fonte nei formati APA, MLA, Chicago, Harvard e in molti altri stili