Cette recherche explore le processus évaluatif tel qu'il se développe dans les disciplines scientifiques au collège, à l'initiative de professeurs. L'originalité et la nouveauté de cette investigation sont de focaliser les élèves dans les interactions évaluatives, inhérentes au processus évaluatif. L'enjeu est de contribuer à l'intelligibilité des comportements des élèves, c'est-à-dire d'expliquer et de justifier leurs actions et leurs réactions au comportement évaluatif du professeur. Alors que, dans les recherches antérieures, le comportement évaluatif du professeur est largement expliqué par ses intentions évaluatives et ses postures d'évaluateur, les travaux et les études ne donnent que très peu d'éléments concernant les élèves. Dans ce contexte : primo, l'existence d'un comportement d'un élève engagé dans une situation d'évaluation est postulé ; secundo, la notion de conscience évaluative individuelle d'un élève est proposée pour rendre compte de son comportement évaluatif et affirmer l'existence de l'élève-évalué ; tertio, l'étude des interactions évaluatives est menée à travers l'investigation et la caractérisation des écarts entre les intentions évaluatives du professeur-évaluateur et la conscience évaluative individuelle de chaque élève-évalué. La méthodologie mise au point a comme premier objectif de vérifier l'existence des intentions évaluatives et de la conscience évaluative, puis comme second objectif d'en étudier les écarts éventuels. Les études de cas sont adaptées à ces deux objectifs : les cas retenus sont des situations d'évaluation formelle particulières, organisées à l'initiative d'un professeur. Dix études de cas et une étude de cas multiples sont menées : les données ont été recueillies auprès de neuf professeurs, enseignant dans trois collèges différents de deux académies ; cent cinq élèves ont été sollicités, répartis dans cinq classes (4 classes de 5ème et 1 classe de 4ème). L'investigation, d'un point de vue didactique, privilégie les contenus de l'enseignement, le contrat et la négociation didactiques, les tâches prescrites. En effet, la place de ces concepts est centrale dans une situation d'évaluation parce que les acteurs - professeur et élèves - en ont une « compréhension symétrique » : cette bivalence en fait des outils permettant la comparaison des intentions évaluatives du professeur-évaluateur et de la conscience évaluative individuelle de chaque élève-évalué. Ces trois concepts apparaissent intriqués dans une situation d'évaluation formelle et y interfèrent en tant que système : dans toute situation d'évaluation formelle, aucun des trois éléments ne peut exister indépendamment des deux autres d'une part, et ce système est systématiquement présent d'autre part. En conclusion, cette recherche exploratoire montre l'existence de la conscience évaluative individuelle des élèves engagés dans une situation d'évaluation formelle. La corrélation entre les intentions évaluatives et la conscience évaluative est marquée par la présence d'écarts qui se manifestent dans le sens donné respectivement par le professeur et chacun de ses élèves, aux contenus de l'enseignement, au contrat didactique et aux tâches prescrites, globalement à l'ensemble des trois, considéré en tant que système. Ces écarts interrogent d'une façon inédite la fiabilité d'une situation d'évaluation formelle pour chaque élève et donc les inférences évaluatives induites. Cette recherche met surtout en lumière que l'élève est un acteur-clé de la situation d'évaluation formelle et pas seulement l'objet de l'évaluation à travers sa production. / This research explores the evaluative process as it is developing in science subjects at middle schools on the teachers' initiative. The originality and the novelty of this study consist of the focus on students in the evaluative interactions inherent in the evaluative process. The aim is to contribute to the intelligibility of students' behaviours, i.e. to explain and to justify the factors that affect student overall actions and reactions to the teacher's evaluative behaviour. While the teacher's evaluative behaviour has been largely explained in previous researches through his or her evaluative intentions and position as an evaluator educational literature has not yet collected sufficient data as regards student characteristics. In this context this investigation examines three interrelated topics denoted as follows. First, the existence of a behaviour characterising students involved in an evaluation situation is postulated. Second, the concept of individual evaluative awareness is proposed in order to take into greater account his or her evaluative behaviour and to establish the existence of the evaluated-student as equally effective. Third, the evaluative interactions are examined through the investigation and the characterisation of divergences between the evaluative intentions of the teacher-evaluator and the individual evaluative awareness of each evaluated-student. With the help of some new methodological approach, the primary goal is to explicit the existence of both evaluative intentions and evaluative awareness, and the second objective is to examine their potential divergences. The case studies are appropriate to these two objectives: the cases presented are specific formal evaluation situations organized to teacher's initiative. Ten case studies and a multiple case study have been carried out: data were collected from nine teachers teaching in three different middle schools belonging to two regional education academies; one hundred five students were contacted throughout five classes (4 classes of "5ème" and 1 class of "4ème", respectively 4 classes of 7th grade and 1 class of 8th grade). From a didactic perspective the investigation focuses on curricular contents, the didactic contract and negotiation, the tasks assigned. These concepts definitely hold a central place in any evaluation situation because the proficient users - teacher and students - have a "symmetrical understanding" of it: this bivalence produces tools for the comparison of the evaluator-teacher's evaluative intentions and the evaluated-student's evaluative awareness. These three concepts intertwined in a formal evaluation situation and conjugate as a system: in any formal evaluation situation, none of the three elements can exist independently from the two others on the one hand, and this system is always present on the second hand. In conclusion, this exploratory research shows the existence of the student individual evaluative awareness when involved in a formal evaluation situation. The correlation between the evaluative intentions and the evaluative awareness is defined by the presence of divergences that emerge concerning under the meaning given respectively by the teacher and each student to the curricular contents, the didactic contract and didactic negotiation, the tasks assigned, globally to the combination of the three concepts regarded as a system. These divergences call into question in an unprecedented manner the finality of a formal evaluation situation for each student and thus the evaluative inferences induced. This research more specifically highlights the idea that the student is a key-player of the formal evaluation situation and not only the object of the evaluation through his or her performance.

Nous présentons dans ce travail de thèse des approches pour la spécification et la vérificationdes systèmes temporisés. La première partie concerne une méthode de spécification enutilisant les diagrammes états-transitions pour modéliser un système donné en partant d’unedescription textuelle. Cette méthode guide l’utilisateur pour le développement de la modélisation.Elle comporte plusieurs étapes et utilise des observateurs d’états et des événements afind’engendrer le diagramme états-transitions. Un outil qui implémente les différentes étapes de laméthode de spécification pour une application semi-automatique est présenté. La seconde partieconcerne une traduction des diagrammes états-transitions vers les réseaux de Petri colorés, cequi permet d’utiliser les méthodes de vérification. Nous prenons en considération dans cette traductionun ensemble important des éléments syntaxiques des diagrammes états-transitions, telsque la concurrence, la hiérarchie, etc. Un outil qui implémente la traduction pour un passageautomatique des diagrammes états-transitions vers les réseaux de Petri colorés est en cours de développement.La dernière partie concerne l’intégration des contraintes temporelles dans les deuxapproches précédentes. Nous définissons des annotations pour les diagrammes états-transitionsdont nous fournissons la syntaxe et la sémantique. Ces annotations seront ensuite utilisées dansla méthode de spécification et la traduction. Le but est de proposer des annotations faciles àcomprendre et à utiliser avec une syntaxe qui prend en compte des contraintes parmi les plusutilisées. / In order to specify and verify timed systems, we present in this thesis approaches using UMLstate machines and coloured Petri nets. Our first approach is a specification method that takesinto account a textual description of the system and generates the corresponding state machinediagram. This method helps a non-expert user to model a system in a structural way. We presenta tool that implements the specification method. Our second approach is the translation of UMLstate machine diagrams to coloured Petri nets diagrams. In this approach we take into account animportant set of UML state machine elements that allows the modelling of concurrent systems,etc. A tool that implements the approach and allows us to automate the translation is beingdeveloped. Finally, the last approach is the integration of time constraints in our specificationmethod and in our translation. We propose a set of annotations to model time in state machinediagrams, and we define the corresponding syntax and semantics.

La SNCF cherche à mettre en place des solutions innovantes permettant d’améliorer la sécurité et les conditions de travail des chargés d’études lors des travaux d’automatisation. En partant de l’étude théorique du projet jusqu’à sa validation sur site, en passant par la mise en œuvre des programmes, du câblage des armoires, et de leur vérification sur plateforme et en usine, ces différentes tâches s’avèrent souvent être longues, complexes, et répétitives, ce qui a pour effet d’augmenter la charge de travail des chargés d’études. En vue d’améliorer les conditions de travail des chargés d’études, ce projet de recherche vise principalement à améliorer leurs méthodologies de vérification des programmes API (aspects fonctionnels et sécuritaires) et du câblage des armoires électriques. Ce projet intitulé « Vérification formelle et simulation pour la validation des programmes API des EALE » se décompose en deux axes :  la vérification hors ligne des programmes API : basée sur une approche formelle, la méthode s’appuie sur une modélisation de l’installation électrique, des programmes API et du cahier de recette dans le model-checker Uppaal. Le principe consiste à vérifier automatiquement si les programmes satisfont aux tests du cahier de recette.  la vérification en ligne du câblage des armoires de contrôle/commande/ protection grâce à un simulateur de partie opérative interfacé avec les armoires de contrôle/commande/protection (via une armoire de test). La vérification se fera de manière automatique et en ligne, toujours avec les tests du cahier de recette, et permettra de valider le câblage des armoires et les réglages des appareils de protection numérique. / In order to keep its leadership in French rail market and to improve working conditions of its systems engineers during automation projects, the SNCF (French acronym for National Society of French Railways) wants to develop solutions increasing the productivity. One of these improvements focuses on the current methodology used by the systems engineers to verify and validate the control command system of electrical installations. This task remains one of the most important during an automation project because it is supposed to ensure installations safety, but it should be optimized. Through an industrial thesis financed by SNCF, the aim of this research project is to improve this method and reduce time validation of control command system by providing tools which will help systems engineers to verify and validate quickly and automatically the control command system during any automation project. It is composed of two axes : - Offline verification of PLC programs with model checking - Online validation of electrical cabinets with virtual commissioning

Omniprésents, la relation homme-machine est encore une définition ardue à cerner. Les ordinateurs réalisent dans le temps des tâches récurrentes. Ils aident ainsi l'homme à manipuler d'énormes quantités de données, souvent même plus rapidement et plus précisément que lui. Malgré cela, la capacité des ordinateurs demeure limitée lorsqu'il s'agit d'extraire automatiquement des informations d'images ou de vidéos, qui représentent pourtant des volumes de données extrêmement importants. La vision par ordinateur est un domaine qui inclut des méthodes d'acquisition, de traitement, d'analyse et de compréhension des images afin de produire de l'information numérique ou symbolique. Un axe de recherche contribuant au développement de ce domaine consiste à reproduire les capacités de la vision humaine par voie électronique afin de percevoir et de comprendre une image. Il s'agit de développer des algorithmes qui reproduisent une des capacités les plus étonnantes du cerveau humain à savoir la déduction des propriétés du monde purement externe au moyen de la lumière qui nous revient des divers objets qui nous entourent. Nos travaux de thèse s'inscrivent dans cet axe de recherche. Nous proposons plusieurs contributions originales s'inscrivant dans le cadre de résolution des problèmes de la reconnaissance et de la localisation des symboles graphiques en contexte. L'originalité des approches proposées réside dans la proposition d'une alliance intéressante entre l'Analyse Formelle de Concepts et la vision par ordinateur. Pour ce faire, nous nous sommes confrontés à l'étude du domaine de l'AFC et plus précisément l'adaptation de la structure du treillis de concepts et son utilisation comme étant l'outil majeur de nos travaux. La principale particularité de notre travail réside dans son aspect générique vu que les méthodes proposées peuvent être alliées à divers outils autre que le treillis de concepts en gardant les mêmes stratégies adoptées et en suivant une procédure semblable. Notre incursion dans le domaine de l'Analyse Formelle de Concepts et plus précisément notre choix de la structure du treillis de Galois appelé aussi treillis de concepts est motivé par les nombreux avantages présentés par cet outil. Le principal avantage du treillis de concepts est l'aspect symbolique qu'il offre. Il présente un espace de recherche concis, précis et souple facilitant ainsi la prise de décision. Nos contributions sont inscrites dans le cadre de la reconnaissance et de localisation de symboles dans les documents graphiques. Nous proposons des chaînes de traitement s'inscrivant dans le domaine de la vision par ordinateur / Computer vision is a field that includes methods for the acquisition, processing, analysis and understanding of images to produce numerical or symbolic information. A research contributing to the development of this area is to replicate the capabilities of human vision to perceive and understand images. Our thesis is part of this research axis. We propose several original contributions belonging to the context of graphics recognition and spotting context. The originality of the proposed approaches is the proposal of an interesting alliance between the Formal Concept Analysis and the Computer Vision fields. We face the study of the FCA field and more precisely the adaptation of the structure of concept lattice and its use as the main tool of our work. The main feature of our work lies in its generic aspect because the proposed methods can be combined with various other tools keeping the same strategies and following a similar procedure. Our foray into the area of the Formal Concept Analysis and more precisely our choice of the structure of the Galois lattice, also called concept lattice is motivated by the many advantages offered by this tool. The main advantage of concept lattice is the symbolic aspect. It is a concise, accurate and flexible search space thus facilitating decision making. Our contributions are recorded as part of the recognition and localization of symbols in graphic documents. We propose to recognize and spot symbols in graphical documents (technical drawings for example) using the alliance between the bag of words representation and the Galois lattice formalism. We opt for various methods belonging to the computer vision field

Cette thèse présente des techniques efficaces pour déléguer des obligations de preuves TLA+ dans des démonstrateurs automatiques basées sur la logique du premier ordre non-sortée et multi-sortée. TLA+ est un langage formel pour la spécification et vérification des systèmes concurrents et distribués. Sa partie non-temporelle basée sur une variante de la théorie des ensembles Zermelo-Fraenkel permet de définir des structures de données. Le système de preuves TLAPS pour TLA+ est un environnement de preuve interactif dans lequel les utilisateurs peuvent vérifier de manière déductive des propriétés de sûreté sur des spécifications TLA+. TLAPS est un assistant de preuve qui repose sur les utilisateurs pour guider l’effort de preuve, il permet de générer des obligations de preuve puis les transmet aux vérificateurs d’arrière-plan pour atteindre un niveau satisfaisant d’automatisation. Nous avons développé un nouveau démonstrateur d’arrière-plan qui intègre correctement dans TLAPS des vérificateurs externes automatisés, en particulier, des systèmes ATP et solveurs SMT. Deux principales composantes constituent ainsi la base formelle pour la mise en oeuvre de ce nouveau vérificateur. Le premier est un cadre de traduction générique qui permet de raccorder à TLAPS tout démonstrateur automatisé supportant les formats standards TPTP/ FOF ou SMT-LIB/AUFLIA. Afin de coder les expressions d’ordre supérieur, tels que les ensembles par compréhension ou des fonctions totales avec des domaines, la traduction de la logique du premier ordre repose sur des techniques de réécriture couplées à une méthode par abstraction. Les théories sortées telles que l’arithmétique linéaire sont intégrés par injection dans la logique multi-sortée. La deuxième composante est un algorithme pour la synthèse des types dans les formules (non-typées) TLA+. L’algorithme, qui est basé sur la résolution des contraintes, met en oeuvre un système de type avec types élémentaires, similaires à ceux de la logique multi-sortée, et une extension avec des types dépendants et par raffinement. Les informations de type obtenues sont ensuite implicitement exploitées afin d’améliorer la traduction. Cette approche a pu être validé empiriquement permettant de démontrer que les vérificateurs ATP/SMT augmentent de manière significative le développement des preuves dans TLAPS / This thesis presents effective techniques for discharging TLA+ proof obligations to automated theorem provers based on unsorted and many-sorted first-order logic. TLA+ is a formal language for specifying and verifying concurrent and distributed systems. Its non-temporal fragment is based on a variant of Zermelo-Fraenkel set theory for specifying the data structures. The TLA+ Proof System TLAPS is an interactive proof environment in which users can deductively verify safety properties of TLA+ specifications. While TLAPS is a proof assistant that relies on users for guiding the proof effort, it generates proof obligations and passes them to backend verifiers to achieve a satisfactory level of automation. We developed a new back-end prover that soundly integrates into TLAPS external automated provers, specifically, ATP systems and SMT solvers. Two main components provide the formal basis for implementing this new backend. The first is a generic translation framework that allows to plug to TLAPS any automated prover supporting the standard input formats TPTP/FOF or SMT-LIB/AUFLIA. In order to encode higher-order expressions, such as sets by comprehension or total functions with domains, the translation to first-order logic relies on term-rewriting techniques coupled with an abstraction method. Sorted theories such as linear integer arithmetic are homomorphically embedded into many-sorted logic. The second component is a type synthesis algorithm for (untyped) TLA+ formulas. The algorithm, which is based on constraint solving, implements one type system for elementary types, similar to those of many-sorted logic, and an expansion with dependent and refinement types. The obtained type information is then implicitly exploited to improve the translation. Empirical evaluation validates our approach: the ATP/SMT backend significantly boosts the proof development in TLAPS

Des familles de logiciels similaires proviennent fréquemment de pratiques de réutilisation de clones de logiciels existants, qui sont ensuite enrichis ou dépouillés de fonctionnalités pour suivre de nouvelles exigences. Avec le temps, ces variantes se multiplient et se complexifient, et il devient difficile de les maintenir, de les faire évoluer. L’ingénierie des lignes de produits logiciels regroupe un ensemble de méthodes visant à faciliter le développement et la gestion de telles collections de logiciels similaires. Documenter la variabilité est le point central de ce paradigme ; on la représente à travers des modèles de variabilité, qui servent de supports à la grande majorité des processus propres à l’ingénierie des lignes de produits. La migration complète ou partielle de ces familles de logiciels vers des approches de type lignes de produits permet la simplification de leur exploitation. La rétro-ingénierie, la modélisation et la gestion de la variabilité sont reconnues comme une phase cruciale et ardue de cette migration. Par conséquent, de nombreuses approches ont été proposées pour étudier des descriptions de familles de logiciels dans ce but. Plusieurs d’entre elles s’appuient sur l’analyse formelle de concepts, un cadre mathématique de groupement hiérarchique qui organise un ensemble d’objets et leurs descriptions dans une structure canonique mettant naturellement en évidence leurs aspects communs et variables.Dans ce manuscrit, nous défendons l'idée que l’analyse formelle de concepts, plus qu’un outil, offre un véritable cadre structurel et réutilisable à l’étude de la variabilité des familles de produits.Dans un premier temps, nous établissons un panorama des informations sur la variabilité qui sont mises en évidence grâce à ce formalisme, et discutons de son spectre d’applicabilité. Nous étudions les points communs entre les structures conceptuelles produites par l’analyse formelle de concepts et les modèles de variabilité. Dans un second temps, nous illustrons l’utilisation originale de ces structures conceptuelles comme support à des opérations de conception et de recherche d’informations. Enfin, nous élargissons notre champ d’étude aux informations plus complexes définies par des modèles de variabilité qui ont été étendus pour en améliorer l’expressivité, et dont la rétro-ingénierie est encore peu étudiée à ce jour. Nous montrons comment certaines propriétés de l’analyse formelle de concepts permettent de généraliser son utilisation à des descriptions de variantes plus complexes, et étudions son application pour la manipulation d’attributs multivalués et de cardinalités, en complément des caractéristiques booléennes traditionnelles. Nous évaluons notre approche sur des données issues de dépôts tels que SPLOT, fork-insight et de matrices de comparaison de produits de wikipedia. / Software families often rise from reuse practices as cloning existing software products which are then enhanced or pruned to fulfill new requirements. With time, these variants grow in number and in complexity, and become more and more complex to maintain. Software product line engineering gathers a set of methods that aims at facilitating the management and development of such collections of existing variants. Documenting variability is the central point of this paradigm; This variability is represented in variability models that support a large part of software product line engineering processes.The partial or complete migration from software families to a product line approach eases their exploitation.Reverse-engineering, modeling and managing variability are known as crucial tasks of the migration: therefore, numerous methods have been proposed to study descriptions of software families for this goal.Some of them are based on formal concept analysis, a mathematical framework for hierarchical clustering which organises set of objects and their descriptions in canonical structures highlighting naturally their commonalities and variability.In this thesis, we defend that formal concept analysis, more than a tool, is a relevant structural, reusable and extensible framework to study variability of software families.First, we propose an overview of variability information which is highlighted thanks to this framework, and we discuss its scope of applicability.We study the common points between the conceptual structures of formal concept analysis and variability models.Then, we show how to use these conceptual structures to support research and modeling operations.Finally, we broaden the scope of this study to take into account more complex information about extended variability.We evaluate our method on data taken from the SPLOT repository, fork-insight and product comparison matrices from wikipedia.

Les architectures de systèmes à logiciel posent des défis pour les experts de sécurité. nombreux travaux ont eu pour objectif d’élaborer des solutions théoriques, des guides méthodologiques et des recommandations, pour renforcer la sécurité et protéger ces systèmes.Une solution proposée est d’intégrer des patrons de sécurité comme solutions méthodologiques à adapter aux spécificités des architectures considérées. Une telle solution est considérée fiable si elle résout un problème de sécurité sans affecter les exigences du système.Une fois un modèle d’architecture implante les patrons de sécurisé, il est nécessaire de valider formellement ce nouveau modèle au regard des exigences attendues. Les techniques de model checking permettent cette validation en vérifiant, d’une part, que les propriétés des patrons de sécurité sont respectées et, d’autre part, que les propriétés du modèle initial sont préservées.Dans ce travail de thèse, nous étudions les méthodes et les concepts pour générer des modèles architecturaux respectant des exigences de sécurité spécifiques. Àpartir d’un modèle d’architecture logicielle, d’une politique de sécurité et d’une librairie des patrons de sécurité, nous souhaitons générer une architecture sécurisée. Chaque patron de sécurité est décrit par une description formelle de sa structure et de son comportement, ainsi qu’une description formelle des propriétés de sécurité associées à ce patron.Cette thèse rend compte des travaux sur l’exploitation de techniques de vérification formelle des propriétés, par model-checking. L’idée poursuivie est de pouvoir générer un modèle d’architecture qui implante des patrons de sécurité, et de vérifier que les propriétés de sécurité, comme les exigences de modèle, sont respectées dans l’architecture résultante.En perspective, les résultats de notre travail pourraient s'appliquer à définir une méthodologie pour une meilleure validation de la sécurité des systèmes industriels comme les SCADA. / Software-based architectures pose challenges for security experts. Many studieshave aimed to develop theoretical solutions, methodological guides and recommendations to enhance security and protect these systems.One solution proposed is to integrate security patterns as methodological solutions to adapt to the specificities of the considered architectures. Such a solution is considered reliable if it solves a security problem without affecting systemrequirements. Once an architecture model implements the security patterns, it is necessary to formally validate this new model against the expected requirements. Model checking techniques allow this validation by verifying, on one hand, that theproperties of the security patterns are respected and, on the other hand, that the properties of the initial model are preserved.In this thesis work, we study the methods and concepts to generate architectural models that meet specific security requirements. Starting with a software architecture model, a security policy and a library of security patterns, we want to generate a secure architecture. Each security pattern is described by aformal description of its structure and behavior, as well as a formal description of the security properties associated with that pattern.This thesis reports work on the technical exploitation of formal verification of properties, using model-checking.The idea is to be able to generate an architecture model that implements security patterns, and to verify that the security properties, as well as the model requirements, are respected in the resulting architecture.In perspective, the results of our work could be applied to define a methodology for a better validation of the security of industrial systems like SCADA.

L’intérêt porté aux algorithmes probabilistes est, entre autres,dû à leur simplicité. Cependant, leur analyse peut devenir très complexeet ce particulièrement dans le domaine du distribué. Nous mettons en évidencedes algorithmes, optimaux en terme de complexité en bits résolvantles problèmes du MIS et du couplage maximal dans les anneaux, qui suiventle même schéma. Nous élaborons une méthode qui unifie les résultatsde bornes inférieures pour la complexité en bits pour les problèmes duMIS, du couplage maximal et de la coloration. La complexité de ces analysespouvant facilement mener à l’erreur et l’existence de nombreux modèlesdépendant d’hypothèses implicites nous ont motivés à modéliserde façon formelle les algorithmes distribués probabilistes correspondant ànotre modèle (par passage de messages, anonyme et synchrone), en vuede prouver formellement des propriétés relatives à leur analyse. Pour cela,nous développons une bibliothèque, RDA, basée sur l’assistant de preuveCoq. / Probabilistic algorithms are simple to formulate. However, theiranalysis can become very complex, especially in the field of distributedcomputing. We present algorithms - optimal in terms of bit complexityand solving the problems of MIS and maximal matching in rings - that followthe same scheme.We develop a method that unifies the bit complexitylower bound results to solve MIS, maximal matching and coloration problems.The complexity of these analyses, which can easily lead to errors,together with the existence of many models depending on implicit assumptionsmotivated us to formally model the probabilistic distributed algorithmscorresponding to our model (message passing, anonymous andsynchronous). Our aim is to formally prove the properties related to theiranalysis. For this purpose, we develop a library, called RDA, based on theCoq proof assistant.

Comme tout logiciel, les compilateurs, et tout particulièrement les compilateurs optimisant, peuvent être défectueux. Il est donc possible qu'ils changent la sémantique du programme compilé, et par conséquent ses propriétés. Dans le cadre de développement de logiciels critiques, où des méthodes formelles sont utilisées pour s'assurer qu'un programme satisfait certaines propriétés, et cela avant qu'il soit compilé, cela pose un problème de fond. Une solution à ce problème est de vérifier le compilateur en s'assurant qu'il préserve la sémantique des programmes compilés. Dans cette thèse, nous évaluons une méthode nouvelle pour développer des passes de compilations sûres: la vérification formelle de validateurs de traduction. D'une part, cette méthode utilise la vérification formelle à l'aide d'assistant de preuve afin d'offrir le maximum de garanties de sûreté sur le compilateur. D'autre part, elle repose sur l'utilisation de la validation de traduction, où chaque exécution du compilateur est validée a posteriori, une méthode de vérification plus pragmatique qui a permis de vérifier des optimisations avancées. Nous montrons que cette approche nouvelle du problème de la vérification de compilateur est viable, et même avantageuse dans certains cas, à travers quatre exemples d'optimisations réalistes et agressives: le list scheduling, le trace scheduling, le lazy code motion et enfin le software pipelining.

La constitution des compétences dans le secteur de l'artisanat est au coeur de la confrontation entre les formes traditionnelles et les formes modernes de l'organisation productive. S'appuyant sur « l'économie des conventions », cette recherche se focalise sur la formation professionnelle qui passe tant par l'apprentissage sur le tas, régulé par les institutions traditionnelles, que par des formations structurées, publiques et privées, résidentielles et en alternance. Repartant de l'ancrage historique de l'artisanat et analysant le positionnement de la formation traditionnelle dans un espace social qui associe fortement cette dernière à l'échec scolaire, la première partie rend compte de l'articulation entre plusieurs régimes d'action collective en matière de qualifications : domestique, professionnel, industriel et marchand. Outre des entretiens auprès des protagonistes des diverses modalités de formation, la seconde partie mobilise une enquête originale auprès de 150 maîtres et ouvriers artisans des métiers de la coiffure et de la coupe-couture menée à Marrakech. Les analyses de données permettent de dégager différentes typologies : sur les choix de formation et de recrutement des maîtres, sur les raisons de l'orientation des ouvriers vers telle ou telle modalité de formation ainsi que sur l'appréciation qu'ils font du contenu des formations structurées et enfin sur les configurations productives résultant des appariements entre maîtres et ouvriers. Il en ressort que par delà la classique distinction « traditionnel versus moderne », la convention domestique, certes prédominante, peut s'associer à des modalités marchandes ou industrielles de gestion des compétences. De même, une configuration professionnelle, fortement liée au recours à la formation structurée, peut également se combiner avec des régulations marchandes ou domestiques. Ces diverses compositions montrent que plusieurs formes de modernité sont susceptibles de se développer et incitent à réinterroger les fondements de l'action collective en matière de qualification et de compétences dans le secteur de l'artisanat.