Spelling suggestions: "subject:"types dde données"" "subject:"types dee données""
1 |
Abstraction techniques for verification of concurrent systems / Techniques d'abstraction dans la verification des systèmes concurrentsEnea, Constantin 08 January 2008 (has links)
Comme les syst`emes mat´eriels et logiciels grandissent de fa¸con continue en ´echelle et fonctionnalit´es, la probabilit´e d’erreurs subtiles de- vient toujours plus grande. Les techniques d’abstraction, souvent bas´ees sur l’interpr´etation abstraite de Cousot, fournissent une m´ethode pour ex´ecuter symboliquement les syst`emes en utilisant le domaine abstrait `a la place du domaine concret. Dans cette th`ese, on introduit des techniques d’abstraction pour les logiques sous des interpr´etations multi-valu´ees. Beaucoup d’applications des logiques multi-valu´ees ont ´et´e trouv´ees dans la v´erification du mat´eriel et du logiciel. Pour la v´erification du mat´eriel, des outils de simulation et des r´ealisations des circuits multi-valu´es v´eritables ont ´et´e propos´es, les risques dynamiques ont ´et´e model´es en introduisant des ´etats faux pour trouver des r´egions chevauchantes des signaux en concurrence, etc. Pour la v´erification du logiciel on a besoin d’incertitude parce qu’on ne peut savoir si certains comportements devraient ˆetre possibles et on a besoin du d´esaccord parce que l’on peut avoir des acteurs diff´erents qui sont en d´esaccord pour la mani`ere dont les syst`emes devraient se comporter. Les abstractions sont obtenues en appliquant des relations d’´equivalence et apr`es, les symboles pr´edicatifs de la logique sont red´efinis `a s’appliquer cor- rectement aux classes d’´equivalence `a l’aide des politiques d’interpr´etation. On fournit des r´esultats de pr´eservation pour la logique de premier ordre, pour la logique temporelle et pour la logique temporelle de la connaissance. Avant de discuter les abstractions multi-valu´ees pour la logique temporelle, nous pr´esentons une ´etude de cas pour utiliser l’abstraction dans le contexte des mod`eles du contrˆole d’acc`es. Nous fournirons aussi une technique d’abstraction pour les types de do- nn´ees. Cette technique d’abstraction peut ˆetre ´elargie pour les types abstraits de donn´ees. Ici, les abstractions sont appliqu´ees aux sp´ecifications initiales au moyen des ´equations et ils sont appel´es des abstractions ´equationnelles. De plus, la technique d’abstraction pr´esent´ee g´en´eralise et clarifie la nature de beaucoup de techniques d’abstraction trouv´ees dans la litt´erature, telles: la technique de dupliquer les symboles pr´edicatifs, shape analysis, l’abstraction par pr´edicats, l’approche de McMillan, etc. Pour raisonner au sujet des syst`emes dynamiques, on introduit les types de donn´ees dynamiques et on ´etend la m´ethode d’abstraction ant´erieure `a ce cas. Le probl`eme principal qui survient quand on utilise les abstractions est de trouver l’abstraction convenable ou de raffiner une abstraction d´ej`a existante pour en obtenir une meilleure. On prouve que les techniques d’abstraction que nous avons introduites pour les types de donn´ees sous l’interpr´etation 3- valu´ee Kleene, peuvent ˆetre utilis´ees dans une proc´edure de raffinement. De plus, on montre que la proc´edure de raffinement guid´e par contre-exemple est plus efficace quand on l’utilise sous les abstractions ´equationnelles / As the hardware and software systems are growing continuously in scale and functionality, the likelihood of subtle errors becomes greater. Abstraction techniques, often based on abstract interpretation, provide a method for symbolically executing systems using the abstract instead of the concrete domain. In this thesis, we are concerned with abstractions for logics under multi-valued interpretations. Many applications of multi-valued logics have been found in hardware and software verification. For hardware verification, simulation tools and imple- mentations of genuinely multi-valued circuits have been proposed, dynamic hazards have been modeled by introducing pseudo states to find overlapping regions of competing signals, implementation of gates have been verified on the basis of switch level models, etc. For software verification, we need uncer- tainty because we may not know whether some behaviors should be possible, we need disagreement because we may have different stakeholders that dis- agree about how the systems should behave and we need to represent relative importance because some behaviors are essential and others may or may not be implemented. The abstractions are obtained by applying equivalence relations and then, the predicate symbols of the logic are re-defined to work properly on equiva- lence classes by using interpretation policies. We provide preservation results for first-order logic, temporal logic, and temporal logic of knowledge. As a case study, we show how abstraction can be used to solve the safety problem for protection systems which model access control policies. The use of abstraction in the context of data types, is also investigated. This technique scales well from data types to abstract data types. Here, abstractions are applied to initial specifications by means of equations and they are called equationally specified abstractions. Moreover, the abstraction technique we propose generalizes and clarifies the nature of many abstraction techniques found in the literature, such as the technique of duplicating pred- icate symbols, shape analysis, predicate abstraction, McMillan’s approach, etc. To reason about dynamic systems, we introduce dynamic data types and extend the previous abstraction technique to this case. The main problem that arises when using abstraction techniques is to find the suitable abstraction or to refine an already existing abstraction in order to obtain a better one. In this thesis, we prove that the abstraction techniques for data types, under Kleene’s three-valued interpretation, can be used in a refinement procedure. Moreover, we show that the counterexample guided abstraction refinement procedure (CEGAR) works better when used with equationally specified abstractions
|
2 |
Sur les types de données dans les langages logico-fonctionnels : Réécriture et surréduction des graphes admissiblesJanodet, Jean-Christophe 24 January 2000 (has links) (PDF)
Les langages logico-fonctionnels sont des langages de programmation de très haut niveau permettant de définir dans un formalisme unifié des types de données, des fonctions et des prédicats (relations). Plusieurs propositions de langages logico-fonctionnels ont été faites mais toutes se restreignent à des calculs basés sur les termes du premier ordre. Cette restriction permet de programmer avec des types abstraits algébriques mais elle rend difficile la manipulation des structures de données du monde réel, modélisées sous la forme de graphes cycliques. L'objectif de cette thèse est donc d'introduire les graphes cycliques comme structure de données de base des langages logico-fonctionnels. Pour cela, nous voyons les programmes comme des systèmes de réécriture de graphes cycliques et nous étudions les relations de réécriture et de surréduction qu'ils induisent (sémantique opérationnelle). Une propriété importante de la réécriture concerne la confluence : elle exprime le déterminisme des calculs effectués. De nombreux résultats de confluence existent pour la réécriture de termes mais ils ne s'étendent généralement pas aux graphes cycliques. Nous mettons en évidence une classe de graphes cycliques particuliers, les graphes admissibles, pour laquelle nous donnons une preuve de confluence de la réécriture. Concernant la relation de surréduction, nous en proposons une définition puis nous montrons que ce calcul est cohérent et complet par rapport à celui de la réécriture dans le cadre des graphes admissibles. Nous étudions ensuite plusieurs stratégies de réécriture et de surréduction de graphes admissibles, c'est-à-dire des algorithmes permettant d'éliminer des calculs inutiles ou redondants. Nous montrons que nos stratégies sont optimales selon de nombreux critères dépendants des systèmes de réécriture considérés.
|
3 |
Techniques d'abstraction dans la verification des systèmes concurrentsEnea, Constantin 08 January 2008 (has links) (PDF)
Comme les systèmes matériels et logiciels grandissent de façon continue en échelle et fonctionnalités, la probabilité d'erreurs subtiles de- vient toujours plus grande. Les techniques d'abstraction, souvent basées sur l'interprétation abstraite de Cousot, fournissent une méthode pour exécuter symboliquement les systèmes en utilisant le domaine abstrait 'a la place du domaine concret. Dans cette thèse, on introduit des techniques d'abstraction pour les logiques sous des interprétations multivaluées. Beaucoup d'applications des logiques multivaluées ont été trouvées dans la vérification du matériel et du logiciel. Pour la vérification du matériel, des outils de simulation et des réalisations des circuits multivaluées véritables ont été proposés, les risques dynamiques ont été modelés en introduisant des 'états faux pour trouver des régions chevauchantes des signaux en concurrence, etc. Pour la vérification du logiciel on a besoin d'incertitude parce qu'on ne peut savoir si certains comportements devraient être possibles et on a besoin du désaccord parce que l'on peut avoir des acteurs différents qui sont en désaccord pour la manière dont les systèmes devraient se comporter. Les abstractions sont obtenues en appliquant des relations d''équivalence et après, les symboles prédicatifs de la logique sont redéfinis 'a s'appliquer cor- correctement aux classes d''équivalence 'a l'aide des politiques d'interprétation. On fournit des résultats de préservation pour la logique de premier ordre, pour la logique temporelle et pour la logique temporelle de la connaissance. Avant de discuter les abstractions multivaluées pour la logique temporelle, nous présentons une 'étude de cas pour utiliser l'abstraction dans le contexte des modèles du contrôle d'accès. Nous fournirons aussi une technique d'abstraction pour les types de données. Cette technique d'abstraction peut être 'élargie pour les types abstraits de données. Ici, les abstractions sont appliquées aux spécifications initiales au moyen des 'équations et ils sont appelés des abstractions 'équationnelles. De plus, la technique d'abstraction présentée généralise et clarifie la nature de beaucoup de techniques d'abstraction trouvées dans la littérature, telles: la technique de dupliquer les symboles prédicatifs, shape analysis, l'abstraction par prédicats, l'approche de McMillan, etc. Pour raisonner au sujet des systèmes dynamiques, on introduit les types de données dynamiques et on étend la méthode d'abstraction antérieure 'a ce cas. Le problème principal qui survient quand on utilise les abstractions est de trouver l'abstraction convenable ou de raffiner une abstraction déjà existante pour en obtenir une meilleure. On prouve que les techniques d'abstraction que nous avons introduites pour les types de données sous interprétation 3- valu'ee Kleene, peuvent être utilisées dans une procédure de raffinement. De plus, on montre que la procédure de raffinement guide par contre-exemple est plus efficace quand on l'utilise sous les abstractions 'équationnelles.
|
4 |
Preuves, Types et Sous-typesRuyer, Frédéric 30 November 2006 (has links) (PDF)
Cette thèse porte sur l'étude théorique et pratique d'un système de typage appliqué à la preuve de programmes de style fonctionnels. Le système de base est le système ST créé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu non-algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types, en construisant une axiomatique basée sur les treillis permettant de modéliser le calcul et la logique. Nous étudions sur cette base le système de types, montrons la réduction du sujet, et la possibilité de définir en interne la normalisabilité et la réductibilité des programmes. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches inspirés des langages fonctionnels - y incluant notamment un système de modules du premier ordre- dans le Lambda-Calcul, et montrons qu'ils s'intègrent harmonieusement dans le système; la méthodologie développée dans cette partie permet d'étendre le langage de types et le langage de programmation en conservant un critère de consistance assurant la sûreté du code typé.
|
5 |
Cohérence à terme fiable avec des types de données répliquées / Dependable eventual consistency with replicated data typesZawirski, Marek 14 January 2015 (has links)
Les bases de données répliquées cohérentes à terme récentes encapsulent la complexité de la concurrence et des pannes par le biais d'une interface supportant la cohérence causale, protégeant l'application des problèmes d'ordre, et/ou des Types de Données Répliqués (RDTs), assurant une sémantique convergente des mises-à-jour concurrentes en utilisant une interface objet. Cependant, les algorithmes fiables pour les RDTs et la cohérence causale ont un coût en terme de taille des métadonnées. Cette thèse étudie la conception de tels algorithmes avec une taille de métadonnées minimisée et leurs limites. Notre première contribution est une étude de la complexité des métadonnées des RDTs. Les nombreuses implémentations existantes impliquent un important surcoût en espace de stockage. Nous concevons un ensemble optimisé et un registre RDTs avec un surcoût des métadonnées réduit au nombre de répliques. Nous démontrons également les bornes inférieures de la taille des métadonnées pour six RDTs, prouvant ainsi l'optimalité de quatre implémentations. Notre seconde contribution est le design de SwiftCloud, une base de données répliquée causalement cohérente d'objets RDTs pour les applications côté client. Nous concevons des algorithmes qui supportent un grand nombre de répliques partielles côté client, s'appuyant sur le cloud, tout en étant tolérant aux fautes et avec une faible taille de métadonnées. Nous démontrons comment supporter la disponibilité (y compris la capacité à basculer entre des centre de données lors d'une erreur), la cohérence et le passage à l'échelle (petite taille de métadonnées, parallélisme) au détriment d'un léger retard dans l'actualisation des données. / Eventually consistent replicated databases offer excellent responsiveness and fault-tolerance, but expose applications to the complexity of concurrency andfailures. Recent databases encapsulate these problems behind a stronger interface, supporting causal consistency, which protects the application from orderinganomalies, and/or Replicated Data Types (RDTs), which ensure convergent semantics of concurrent updates using object interface. However, dependable algorithms for RDT and causal consistency come at a cost in metadata size. This thesis studies the design of such algorithms with minimized metadata, and the limits of the design space. Our first contribution is a study of metadata complexity of RDTs. RDTs use metadata to provide rich semantics; many existing RDT implementations incur high overhead in storage space. We design optimized set and register RDTs with metadata overhead reduced to the number of replicas. We also demonstrate metadata lower bounds for six RDTs, thereby proving optimality of four implementations. Our second contribution is the design of SwiftCloud, a replicated causally-consistent RDT object database for client-side applications. We devise algorithms to support high numbers of client-side partial replicas backed by the cloud, in a fault-tolerant manner, with small metadata. We demonstrate how to support availability and consistency, at the expense of some slight data staleness; i.e., our approach trades freshness for scalability (small metadata, parallelism), and availability (ability to fail-over between data centers). We validate our approach with experiments involving thousands of client replicas.
|
6 |
Méthodologie d'évaluation pour les types de données répliqués / Evaluation methodology for replicated data typesAhmed-Nacer, Mehdi 05 May 2015 (has links)
Pour fournir une disponibilité permanente des données et réduire la latence réseau, les systèmes de partage de données se basent sur la réplication optimiste. Dans ce paradigme, il existe plusieurs copies de l'objet partagé dite répliques stockées sur des sites. Ces répliques peuvent être modifiées librement et à tout moment. Les modifications sont exécutées en local puis propagées aux autres sites pour y être appliquées. Les algorithmes de réplication optimiste sont chargés de gérer les modifications parallèles. L'objectif de cette thèse est de proposer une méthodologie d'évaluation pour les algorithmes de réplication optimiste. Le contexte de notre étude est l'édition collaborative. Nous allons concevoir pour cela un outil d'évaluation qui intègre un mécanisme de génération de corpus et un simulateur d'édition collaborative. À travers cet outil, nous allons dérouler plusieurs expériences sur deux types de corpus: synchrone et asynchrone. Dans le cas d'une édition collaborative synchrone, nous évaluerons les performances des différents algorithmes de réplication sur différents critères tels que le temps d'exécution, l'occupation mémoire, la taille des messages, etc. Nous proposerons ensuite quelques améliorations. En plus, dans le cas d'une édition collaborative asynchrone, lorsque deux répliques se synchronisent, les conflits sont plus nombreux à apparaître. Le système peut bloquer la fusion des modifications jusqu'à ce que l'utilisateur résolut les conflits. Pour réduire le nombre de ces conflits et l'effort des utilisateurs, nous proposerons une métrique d'évaluation et nous évaluerons les différents algorithmes sur cette métrique. Nous analyserons le résultat pour comprendre le comportement des utilisateurs et nous proposerons ensuite des algorithmes pour résoudre les conflits les plus important et réduire ainsi l'effort des développeurs. Enfin, nous proposerons une nouvelle architecture hybride basée sur deux types d'algorithmes de réplication. Contrairement aux architectures actuelles, l'architecture proposéeest simple, limite les ressources sur les dispositifs clients et ne nécessite pas de consensus entre les centres de données / To provide a high availability from any where, at any time, with low latency, data is optimistically replicated. This model allows any replica to apply updates locally, while the operations are later sent to all the others. In this way, all replicas eventually apply all updates, possibly even in different order. Optimistic replication algorithms are responsible for managing the concurrent modifications and ensure the consistency of the shared object. In this thesis, we present an evaluation methodology for optimistic replication algorithms. The context of our study is collaborative editing. We designed a tool that implements our methodology. This tool integrates a mechanism to generate a corpus and a simulator to simulate sessions of collaborative editing. Through this tool, we made several experiments on two different corpus: synchronous and asynchronous. In synchronous collaboration, we evaluate the performance of optimistic replication algorithms following several criteria such as execution time, memory occupation, message's size, etc. After analysis, some improvements were proposed. In addition, in asynchronous collaboration, when replicas synchronize their modifications, more conflicts can appear in the document. In this case, the system cannot merge the modifications until a user resolves them. In order to reduce the conflicts and the user's effort, we propose an evaluation metric and we evaluate the different algorithms on this metric. Afterward, we analyze the quality of the merge to understand the behavior of the users and the collaboration cases that create conflicts. Then, we propose algorithms for resolving the most important conflicts, therefore reducing the user's effort. Finally, we propose a new architecture for supporting cloud-based collaborative editing system. This architecture is based on two optimistic replication algorithms. Unlike current architectures, the proposed one removes the problems of the centralization and consensus between data centers, is simple and accessible for any developers
|
7 |
Programmation en lambda-calcul pur et typéNour, Karim 14 January 2000 (has links) (PDF)
Mes travaux de recherche portent sur la théorie de la démonstration, le lambda-calcul et l'informatique théorique, dans la ligne de la correspondance de Curry-Howard entre les preuves et les programmes.<br /><br />Dans ma thèse de doctorat, j'ai étudié les opérateurs de mise en mémoire pour les types de données. Ces notions, qui sont introduites par Krivine, permettent de programmer en appel par valeur tout en utilisant la stratégie de la réduction de tête pour exécuter les $\lambda$-termes. Pour cette étude, j'ai introduit avec David une extension du $\lambda$-calcul avec substitutions explicites appelée $\lambda$-calcul dirigé. Nous en avons déduit une nouvelle caractérisation des termes de mise en mémoire et obtenu des nombreux résultats très fins à leur sujet. En ce qui concerne le typage des opérateurs de mise en mémoire, Krivine a trouvé une formule du second ordre, utilisant la non-non traduction de Gödel de la logique classique dans la logique intuitionniste, qui caractérise ces opérateurs. Je me suis attaché à diverses généralisations du résultat de Krivine pour les types à quantificateur positif dans des extensions de la logique des prédicats du second ordre.<br /><br />J'ai poursuivi, après ma thèse, une activité de recherche sur l'extension de la correspondance de Curry-Howard à la logique classique, au moyen des instructions de contrôle. J'ai étudié des problèmes liés aux types de données dans deux de ces systèmes : le $\lambda \mu$-calcul de Parigot et le $\lambda C$-calcul de Krivine. J'ai donné des algorithmes très simples permettant de calculer la valeur d'un entier classique dans ces deux systèmes. J'ai également caractérisé les termes dont le type est l'une des règles de l'absurde. J'ai étendu le système de Parigot pour en obtenir une version non déterministe mais où les entiers se réduisent toujours en entiers de Church. Curieusement, ce système permet de programmer la fonction ``ou parallèle''.<br /><br />Je me suis intéressé aux systèmes numériques qui servent à représenter les entiers naturels au sein du $\lambda$-calcul. J'ai montré que pour un tel système, la possession d'un successeur, d'un prédécesseur et d'un test à zéro sont des propriétés indépendantes, puis qu'un système ayant ces trois fonctions possède toujours un opérateur de mise en mémoire. Dans un cadre typé, j'ai apporté une réponse négative à une conjecture de Tronci qui énonçait une réciproque du résultat précédent.<br /><br />La notion de mise en mémoire ne s'applique qu'à des types de données. Une définition syntaxique a été donné par Böhm et Berarducci, et Krivine a proposé une définition sémantique de ces types. J'ai obtenu avec Farkh des résultats reliant la syntaxe et la sémantique des types de données. Nous avons proposé également des définitions des types entrée et des types sortie pour lesquelles nous avons montré diverses propriétés syntaxiques et sémantiques.<br /><br />J'ai réussi à combiner la logique intuitionniste et la logique classique en une logique mixte. Dans cette logique, on distingue deux genres de variables du second ordre, suivant que l'on peut, ou non, leur appliquer le raisonnement par l'absurde. Ce cadre m'a permi de donner le type le plus général pour les opérateurs de mise en mémoire. Vu le rôle important que cette logique semble devoir jouer dans la théorie de ces opérateurs, j'en ai mené avec A. Nour une étude théorique approfondie. Le système de logique mixte propositionnelle auquelle nous avons abouti évoque les sytèmes $LC$ de Girard et $LK^{tq}$ de Danos, Joinet et Schellinx.<br /><br />Je me suis intéressé avec David à l'équivalence induite par l'égalité entre les arbres de Böhm infiniment $\eta$-expansés. Avec Raffalli, je me suis également intéressé à la sémantique de la logique du second ordre.
|
Page generated in 0.0559 seconds