La vérification des systèmes d'états finis, qu'ils soient distribués ou concurrents, est confrontée en pratique au problème d'explosion d'états (taille prohibitive de l'espace d'états sous-jacent) qui survient pour des systèmes de taille réaliste, contenant de nombreux processus en parallèle et des structures de données complexes. Différentes techniques ont été proposées pour combattre l'explosion d'états, telles que la vérification à la volée, la réduction d'ordre partiel, ou encore la vérification distribuée. Cependant, l'expérience pratique a montré qu'aucune de ces techniques, à elle seule, n'est toujours suffisante pour maîtriser des systèmes à grande échelle. Cette thèse propose une combinaison de ces approches dans le but de faire passer à l'échelle leurs capacités de vérification. Notre approche est basée sur les Systèmes d'Equations Booléennes (SEBs), qui fournissent une représentation intermédiaire élégante des problèmes de vérification définis sur des Systèmes de Transitions Etiquetées, comme la comparaison par équivalence, la réduction par tau-confluence, l'évaluation de formules de mu-calcul modal sans alternance, ou encore la génération de cas de tests de conformité. Nous proposons DSolve et MB-DSolve, deux nouveaux algorithmes pour la résolution distribuée à la volée de SEBs (contenant un, resp. plusieurs blocs d'équations), et nous les employons comme moteurs de calcul pour quatre outils de vérification à la volée développés au sein de la boîte à outils CADP en utilisant l'environnement OPEN/CAESAR : le comparateur par équivalence BISIMULATOR, le réducteur TAU_CONFLUENCE, l'évaluateur de propriétés temporelles EVALUATOR, et le générateur de cas de tests de conformité EXTRACTOR. Les mesures expérimentales effectuées sur des grappes de machines montrent des accélérations quasi-linéaires et un bon passage à l'échelle des versions distribuées de ces outils par rapport à leurs équivalents séquentiels.

La découpe de viandes et le filetage de poisson, destinés aux rois et aux nobles dans les siècles passés et, plus récemment, aux clients de la restauration traditionnelle, font partie de l’histoire de la gastronomie, au même titre que l’histoire de la cuisine. Ces pratiques, considérées comme une technique ou une science, voire, par certains, comme un art, bien que déjà présentes sous une forme ritualisée dans bien des textes mythologiques et des légendes fondatrices, ont connu plusieurs évolutions historiques. Dès le Moyen Âge, la pratique de la découpe des viandes et poissons auprès des élites s’est éloignée des techniques de la boucherie pour revêtir une dimension artistique. À partir de la Renaissance et jusqu’au XVIIIème siècle, les volailles et autres viandes sont filetées par les écuyers tranchants, véritables spécialistes qui effectuent des gestes empreints d’élégance, tel celui qui consiste à découper les viandes à la volée, maintenues en l’air en haut d’une fourchette. À partir du XVIIIème siècle, la découpe doit s’adapter aux changements sociaux : à la fin de l’Ancien Régime, en France, elle connaît une première grande évolution à la suite de changements radicaux dans la manière de concevoir la cuisine, puis avec l’apparition du service à la russe et la mise en valeur des rôts (pièces rôties) au centre du repas, évolution bientôt suivie par d’autres, en grande partie influencées par Marie-Antoine Carême puis Urbain Dubois et Emile Bernard. Plusieurs transformations sociales, culturelles et professionnelles auront aussi leur importance : la popularisation des sports d’hiver va marquer le déclin du poste de maître d’hôtel ; la loi Godart (juillet 1933) relative au contrôle et à la répartition des pourboires, va cristalliser le fameux conflit cuisine-salle ; par ailleurs, les « commandements de la nouvelle cuisine » prônés par Christian Millau et Henri Gault (1973) imposent la généralisation du service à l’assiette et rendent l’ancienne science du maître d’hôtel obsolète. Mais les pratiques de la découpe sont également présentes dans le foyer familial. De nombreux écrits sur les usages domestiques décrivent la manière de fileter viandes et poissons. Les pères de famille, dits amphitryons, possèdent et transmettent ce savoir-faire à l’occasion des réunions familiales. Traditionnellement, si la mère de famille officie en cuisine, le père de famille gère, en plus des boissons, les découpes de volailles et gigots. Mais, depuis la moitié du XXème siècle, ces usages sont en déclin. Malgré tout, l’art de la découpe a survécu sous forme de technique, dans certains restaurants et dans les écoles hôtelières, où il fait l’objet de débats houleux entre enseignants et professionnels, qui rejouent, à leur manière, la querelle des Anciens et des Modernes. La restauration française, actuellement en difficulté et en recherche de repères, a sans doute beaucoup à gagner de ces travaux sur les découpes et filetages devant les clients. En ce début du XXIème siècle, elle peut y retrouver une authenticité ancrée sur des racines profondes. / The carving tableside of meats, fishes and fruits, dedicated to kings and nobility in past centuries and demonstrated today in some traditional restaurants, is part of the history of gastronomy, as well as food history. Regarded as a technic or a science, or even as an art, this practice already present in a ritualized form in many mythological texts and founding legends, has undergone major changes in history. From the Middle Ages, it has moved away from the butchery techniques to get an artistic dimension. Since the Renaissance era to the eighteenth century, poultry and other meats are carved by real specialists called carving horsemen, who perform gestures imbued with elegance, like the « flying cut » (cutting the meat held in the air on top of a fork). From the eighteenth century, the cut must adapt to social changes at the end of the Old Regime in France, the first major carving art revolution follows radical changes in the way of designing food platers by chefs, then with the appearance of the russian service largely influenced by Marie-Antoine Carême and Urbain Dubois. The roast becomes the center of the meal. Subsequently, several social, cultural and professional changes will take place in the carving history : the popularization of winter sports that will mark the decline of carving station, the Godart law (July 1933), that legislates control of the distribution of tips and will crystallize the famous kitchen/waiting struggle, and finally the « commandments of Nouvelle Cuisine » led by Christian Millau and Henri Gault (1973) which impose the generalization of the plated service and render obsolete the ancient science of the maitre d’. But cutting practices is also found in the family home. Extensive litterature demonstrate how to thread meat and fish for domestic use. Fathers, called amphitryons in France, possess and transmit this knowledge during family gatherings. Traditionally, if the housewife officiates in the kitchen, the father manages, in addition to drinks, the cuts of poultry and legs of lamb. But since the mid-twentieth century, we must recognize that these uses are declining. Still, the art of cutting survived in the technical way, in some restaurants and hospitality schools, where it is subject of heated debate between teachers and professionals, replaying in their own way the quarrel of the Ancients and the Moderns. French restaurants, currently in great difficulty and in search of direction, have probably much to gain from a reflection on the return of threads and cut in front of customers. It would find, in our view, deep roots authenticity in this beginning of the 21st century.

Cette thèse s'intéresse à l'étude des problèmes de diagnostic des fautes sur les systèmes à événements discrets en utilisant les modèles réseau de Petri. Des techniques d'exploration incrémentale et à-la-volée sont développées pour combattre le problème de l'explosion de l'état lors de l'analyse de la diagnosticabilité. Dans le contexte atemporel, la diagnosticabilité de modèles RdP-L est abordée par l'analyse d'une série de problèmes K-diagnosticabilité. L'analyse de la diagnosticabilité est effectuée sur la base de deux modèles nommés respectivement FM-graph et FM-set tree qui sont développés à-la-volée. Un diagnostiqueur peut être dérivé à partir du FM-set tree pour le diagnostic en ligne. Dans le contexte temporel, les techniques de fractionnement des intervalles de temps sont élaborées pour développer représentation de l'espace d'état des RdP-LT pour laquelle des techniques d'analyse de la diagnosticabilité peuvent être utilisées. Sur cette base, les conditions nécessaires et suffisantes pour la diagnosticabilité de RdP-LT ont été déterminées. En pratique, l'analyse de la diagnosticabilité est effectuée sur la base de la construction à-la-volée d'une structure nommée ASG et qui contient des informations relatives à l'occurrence de fautes. D'une manière générale, l'analyse effectuée sur la base des techniques à-la-volée et incrémentale permet de construire et explorer seulement une partie de l'espace d'état, même lorsque le système est diagnosticable. Les résultats des simulations effectuées sur certains benchmarks montrent l'efficacité de ces techniques en termes de temps et de mémoire par rapport aux approches traditionnelles basées sur l'énumération des états / This PhD thesis deals with fault diagnosis of discrete event systems using Petri net models. Some on-the-fly and incremental techniques are developed to reduce the state explosion problem while analyzing diagnosability. In the untimed context, an algebraic representation for labeled Petri nets (LPNs) is developed for featuring system behavior. The diagnosability of LPN models is tackled by analyzing a series of K-diagnosability problems. Two models called respectively FM-graph and FM-set tree are developed and built on the fly to record the necessary information for diagnosability analysis. Finally, a diagnoser is derived from the FM-set tree for online diagnosis. In the timed context, time interval splitting techniques are developed in order to make it possible to generate a state representation of labeled time Petri net (LTPN) models, for which techniques from the untimed context can be used to analyze diagnosability. Based on this, necessary and sufficient conditions for the diagnosability of LTPN models are determined. Moreover, we provide the solution for the minimum delay ∆ that ensures diagnosability. From a practical point of view, diagnosability analysis is performed on the basis of on-the-fly building of a structure that we call ASG and which holds fault information about the LTPN states. Generally, using on-the-fly analysis and incremental technique makes it possible to build and investigate only a part of the state space, even in the case when the system is diagnosable. Simulation results obtained on some chosen benchmarks show the efficiency in terms of time and memory compared with the traditional approaches using state enumeration

No description available.

Cette thèse est dédiée à l’étude de deux familles de problèmes de partition de graphe. Nous considérons tout d’abord le problème de sommet-partitionner un graphe en sous-graphesconnexes. Plus précisément, étant donnés p entiers positifs n1; n2; :::; np dont la somme vautl’ordre d’un graphe G, peut-on partitionner V (G) en p parts V1; V2; :::; Vp de sorte que chaque Vi induise un sous-graphe connexe d’ordre ni ? Nous nous intéressons ensuite à des questions plus fortes. Que peut-on dire si l’on souhaite que G soit partitionnable de cette manière quels que soient p et n1; n2; :::; np ? Si l’on souhaite que des sommets particuliers de G appartiennent à des sous-graphes particuliers de la partition ? Et si l’on souhaite que les sous-graphes induits soient plus que connexes ? Nous considérons toutes ces questions à la fois du point de vue structurel (sous quelles conditions structurelles une partition particulière existe-t-elle nécessairement ?) et algorithmique (est-il difficile de trouver une partition particulière ?).Nous nous intéressons ensuite à la 1-2-3 Conjecture, qui demande si tout graphe G admet une 3-pondération voisin-somme-distinguante de ses arêtes, i.e. une 3-pondération par laquelle chaque sommet de G peut être distingué de ses voisins en comparant uniquement leur somme de poids incidents. Afin d’étudier la 1-2-3 Conjecture, nous introduisons notamment la notionde coloration localement irrégulière d’arêtes, qui est une coloration d’arêtes dont chaque classe de couleur induit un sous-graphe dans lequel les sommets adjacents sont de degrés différents.L’intérêt principal de cette coloration est que, dans certaines situations, une pondération d’arêtes voisin-somme-distinguante peut être déduite d’une coloration d’arêtes localement irrégulière. Nospréoccupations dans ce contexte sont principalement algorithmiques (est-il facile de trouver une pondération d’arêtes voisin-somme-distinguante ou une coloration d’arêtes localement irrégulière utilisant le plus petit nombre possible de poids ou couleurs ?) et structurelles (quel est le plus petit nombre de couleurs d’une coloration d’arêtes localement irrégulière ?). Nous considérons également ces questions dans le contexte des graphes orientés. / This thesis is dedicated to the study of two families of graph partition problems.First, we consider the problem of vertex-partitioning a graph into connected subgraphs.Namely, given p positive integers n1; n2; :::; np summing up to the order of some graph G, canwe partition V (G) into p parts V1; V2; :::; Vp so that each Vi induces a connected subgraph withorder ni? We then consider stronger questions. Namely, what if we want G to be partitionablewhatever are p and n1; n2; :::; np? What if we also want specific vertices of G to belong to somespecific subgraphs induced by the vertex-partition? What if we want the subgraphs induced bythe vertex-partition to be more than connected? We consider all these questions regarding boththe structural (are there structural properties ensuring that a specific vertex-partition necessarilyexists?) and algorithmic (is it hard to deduce a specific vertex-partition?) points of view.Then, we focus on the so-called 1-2-3 Conjecture, which asks whether every graph G admitsa neighbour-sum-distinguishing 3-edge-weighting, i.e. a 3-edge-weighting by which all adjacentvertices of G get distinguished by their sums of incident weights. As a tool to deal with the1-2-3 Conjecture, we notably introduce the notion of locally irregular edge-colouring, which isan edge-colouring in which every colour class induces a subgraph whose adjacent vertices havedistinct degrees. The main point is that, in particular situations, a neighbour-sum-distinguishingedge-weighting of G can be deduced from a locally irregular edge-colouring of it. Our concernsin this context are mostly algorithmic (can we easily find a neighbour-sum-distinguishing edgeweightingor locally irregular edge-colouring using the least number of weights or colours?) andstructural (what is the least number of colours in a locally irregular edge-colouring?). We alsoconsider similar matters in the context of oriented graphs.

Dans les systèmes informatiques, la consommation énergétique est devenue le facteur le plus limitant de la croissance de performance observée pendant les décennies précédentes. Conséquemment, les paradigmes d'architectures d'ordinateur et de développement logiciel doivent changer si nous voulons éviter une stagnation de la performance durant les décennies à venir.Dans ce nouveau scénario, des nouveaux designs architecturaux et micro-architecturaux peuvent offrir des possibilités d'améliorer l'efficacité énergétique des ordinateurs, grâce à la spécialisation matérielle, comme par exemple les configurations de cœurs hétérogènes, des nouvelles unités de calcul et des accélérateurs. D'autre part, avec cette nouvelle tendance, le développement logiciel devra faire face au manque de portabilité de la performance entre les matériels toujours en évolution et à l'écart croissant entre la performance exploitée par les programmeurs et la performance maximale exploitable du matériel. Pour traiter ce problème, la contribution de cette thèse est une méthodologie et la preuve de concept d'un cadriciel d'auto-tuning à la volée pour les systèmes embarqués. Le cadriciel proposé peut à la fois adapter du code à une micro-architecture inconnue avant la compilation et explorer des possibilités d'auto-tuning qui dépendent des données d'entrée d'un programme.Dans le but d'étudier la capacité de l'approche proposée à adapter du code à des différentes configurations micro-architecturales, j'ai développé un cadriciel de simulation de processeurs hétérogènes ARM avec exécution dans l'ordre ou dans le désordre, basé sur les simulateurs gem5 et McPAT. Les expérimentations de validation ont démontré en moyenne des erreurs absolues temporels autour de 7 % comparé aux ARM Cortex-A8 et A9, et une estimation relative d'énergie et de performance à 6 % près pour le benchmark Dhrystone 2.1 comparée à des CPUs Cortex-A7 et A15 (big.LITTLE). Les résultats de validation temporelle montrent que gem5 est beaucoup plus précis que les simulateurs similaires existants, dont les erreurs moyennes sont supérieures à 15 %.Un composant important du cadriciel d'auto-tuning à la volée proposé est un outil de génération dynamique de code, appelé deGoal. Il définit un langage dédié dynamique et bas-niveau pour les noyaux de calcul. Pendant cette thèse, j'ai porté deGoal au jeu d'instructions ARM Thumb-2 et créé des nouvelles fonctionnalités pour l'auto-tuning à la volée. Une validation préliminaire dans des processeurs ARM ont montré que deGoal peut en moyenne générer du code machine avec une qualité équivalente ou supérieure comparé aux programmes de référence écrits en C, et même par rapport à du code vectorisé à la main.La méthodologie et la preuve de concept de l'auto-tuning à la volée dans des processeurs embarqués ont été développées autour de deux applications basées sur noyau de calcul, extraits de la suite de benchmark PARSEC 3.0 et de sa version vectorisée à la main PARVEC.Dans l'application favorable, des accélérations de 1.26 et de 1.38 ont été observées sur des cœurs réels et simulés, respectivement, jusqu'à 1.79 et 2.53 (toutes les surcharges dynamiques incluses).J'ai aussi montré par la simulation que l'auto-tuning à la volée d'instructions SIMD aux cœurs d'exécution dans l'ordre peut surpasser le code de référence vectorisé exécuté par des cœurs d'exécution dans le désordre similaires, avec une accélération moyenne de 1.03 et une amélioration de l'efficacité énergétique de 39 %.L'application défavorable a été choisie pour montrer que l'approche proposée a une surcharge négligeable lorsque des versions de noyau plus performantes ne peuvent pas être trouvées.En faisant tourner les deux applications sur les processeurs réels, la performance de l'auto-tuning à la volée est en moyenne seulement 6 % en dessous de la performance obtenue par la meilleure implémentation de noyau trouvée statiquement. / In computing systems, energy consumption is limiting the performance growth experienced in the last decades. Consequently, computer architecture and software development paradigms will have to change if we want to avoid a performance stagnation in the next decades.In this new scenario, new architectural and micro-architectural designs can offer the possibility to increase the energy efficiency of hardware, thanks to hardware specialization, such as heterogeneous configurations of cores, new computing units and accelerators. On the other hand, with this new trend, software development should cope with the lack of performance portability to ever changing hardware and with the increasing gap between the performance that programmers can extract and the maximum achievable performance of the hardware. To address this issue, this thesis contributes by proposing a methodology and proof of concept of a run-time auto-tuning framework for embedded systems. The proposed framework can both adapt code to a micro-architecture unknown prior compilation and explore auto-tuning possibilities that are input-dependent.In order to study the capability of the proposed approach to adapt code to different micro-architectural configurations, I developed a simulation framework of heterogeneous in-order and out-of-order ARM cores. Validation experiments demonstrated average absolute timing errors around 7 % when compared to real ARM Cortex-A8 and A9, and relative energy/performance estimations within 6 % for the Dhrystone 2.1 benchmark when compared to Cortex-A7 and A15 (big.LITTLE) CPUs.An important component of the run-time auto-tuning framework is a run-time code generation tool, called deGoal. It defines a low-level dynamic DSL for computing kernels. During this thesis, I ported deGoal to the ARM Thumb-2 ISA and added new features for run-time auto-tuning. A preliminary validation in ARM processors showed that deGoal can in average generate equivalent or higher quality machine code compared to programs written in C, including manually vectorized codes.The methodology and proof of concept of run-time auto-tuning in embedded processors were developed around two kernel-based applications, extracted from the PARSEC 3.0 suite and its hand vectorized version PARVEC. In the favorable application, average speedups of 1.26 and 1.38 were obtained in real and simulated cores, respectively, going up to 1.79 and 2.53 (all run-time overheads included). I also demonstrated through simulations that run-time auto-tuning of SIMD instructions to in-order cores can outperform the reference vectorized code run in similar out-of-order cores, with an average speedup of 1.03 and energy efficiency improvement of 39 %. The unfavorable application was chosen to show that the proposed approach has negligible overheads when better kernel versions can not be found. When both applications run in real hardware, the run-time auto-tuning performance is in average only 6 % way from the performance obtained by the best statically found kernel implementations.

Une approche donnant de meilleurs résultats pour les potentiels interatomiques en apprentissage-machine à la volée est proposée en comparant trois approches pour la recherche de processus activés par la technique d'activation-relaxation. Tout d'abord, nous discutons de l'intérêt et des enjeux de l'utilisation des potentiels en apprentissage-machine et justifions l'utilisation de l'apprentissage à la volée pour la recherche de processus activés. Cela nous mène à présenter la forme générale des potentiels en apprentissage-machine, quelques modèles via leurs descripteurs de configuration atomique, paramètres et hyperparamètres ainsi que la méthode de l'apprentissage à la volée. Ensuite, nous présentons les méthodes d'exploration utilisées et les détails d'intégration du potentiel à la volée. Enfin, nous menons une étude comparative des trois approches pour un système de Si et de SiGe avec diffusion de lacune. La méthodologie proposée de potentiel de haute précision permet d'étendre la gamme de problèmes pouvant être étudiés par la technique d'activation-relaxation. / An approach giving better results for on-the-fly machine learning interatomic potential proposed by comparing three approaches for exploration of activated processes by the activationrelaxation technique. We first discuss the interest and challenges of on-the-fly machine learning potential and justify the use of on-the-fly learning for the search for activated processes. This leads us to present the general form of machine learning potentials and some models via their atomic configuration descriptors, parameters and hyperparameters as well as the on-the-fly learning method. Then, the exploration methods used are defined and the details of the integration of the potential are presented. Finally, a study is conducted comparing the three approaches for a Si and SiGe system with vacancy diffusion. The proposed methodology of high-precision potential allows to extend the range of possible problems to be studied by the activation-relaxation technique.