L'être humain fait des erreurs, en particulier dans la réalisation de taches complexes comme la construction des systèmes informatiques modernes. Nous nous intéresserons dans cette thèse à la vérification assistée par ordinateur du bon fonctionnement des systèmes informatiques. Les systèmes informatiques actuels sont de grande complexité. Afin de garantir leur fiabilité, la vérification automatique est une alternative au 'testing' et à la simulation. Elle propose d'utiliser des ordinateurs pour explorer exhaustivement l'ensemble des états du système, ce qui est problématique: même des systèmes assez simples peuvent atteindre un grand nombre d'états. L'utilisation des bonnes représentations des espaces d'états est essentielle pour surmonter la complexité des problèmes posés en vérification automatique. La vérification des systèmes concurrents amène des difficultés additionnelles, car l'analyse doit, en principe, examiner tous les ordres possibles d'exécution des actions concurrentes. Le dépliage des réseaux de Petri est une technique largement étudiée pour la vérification des systèmes concurrents. Il représentent l'espace d'états du système par un ordre partiel, ce qui se révèle aussi naturel qu'efficace pour la vérification automatique. Nous nous intéressons à la vérification des systèmes concurrents modélisés par des réseaux de Petri, en étudiant deux techniques remarquables de vérification: le 'model checking' et le diagnostic. Nous étudions les dépliages des réseaux de Petri étendus avec des arcs de lecture. Ces dépliages, aussi appelés dépliages contextuels, semblent être une meilleure représentation des systèmes contenant des actions concurrentes qui lisent des ressources partagées : ils peuvent être exponentiellement plus compacts dans ces cas. Ce travail contient des contributions théoriques et pratiques. Dans un premier temps, nous étudions la construction des dépliages contextuels, en proposant des algorithmes et des structures de données pour leur construction efficace. Nous combinons les dépliages contextuels avec les 'merged process', une autre représentation des systèmes concurrents qui contourne l'explosion d'états dérivée du non-déterminisme. Cette nouvelle structure, appelée 'contextual merged process', est souvent exponentiellement plus compacte, ce que nous montrons expérimentalement. Ensuite, nous nous intéressons à la vérification à l'aide des dépliages contextuels. Nous traduisons vers SAT le problème d'atteignabilité des dépliages contextuels, en abordant les problèmes issus des cycles de conflit asymétrique. Nous introduisons également une méthode de diagnostic avec des hypothèses d'équité, cette fois pour des dépliages ordinaires. Enfin, nous implémentons ces algorithmes dans le but de produire un outil de vérification compétitif et robuste. L'évaluation de nos méthodes sur un ensemble d'exemples standards, et leur comparaison avec des techniques issues des dépliages ordinaires, montrent que la vérification avec des dépliages contextuels est plus efficace que les techniques existantes dans de nombreux cas. Ceci suggère que les dépliages contextuels, et les structures d'évènements asymétriques en général, méritent une place légitime dans la recherche en concurrence, également du point de vu de leur efficacité. / Humans make mistakes, especially when faced to complex tasks, such as the construction of modern hardware or software. This thesis focuses on machine-assisted techniques to guarantee that computers behave correctly. Modern computer systems are large and complex. Automated formal verification stands as an alternative to testing or simulation to ensuring their reliability. It essentially proposes to employ computers to exhaustively check the system behavior. Unfortunately, automated verification suffers from the state-space explosion problem: even relatively small systems can reach a huge number of states. Using the right representation for the system behavior seems to be a key step to tackle the inherent complexity of the problems that automated verification solves. The verification of concurrent systems poses additional issues, as their analysis requires to evaluate, conceptually, all possible execution orders of their concurrent actions. Petri net unfoldings are a well-established verification technique for concurrent systems. They represent behavior by partial orders, which not only is natural but also efficient for automatic verification. This dissertation focuses on the verification of concurrent systems, employing Petri nets to formalize them, and studies two prominent verification techniques: model checking and fault diagnosis. We investigate the unfoldings of Petri nets extended with read arcs. The unfoldings of these so-called contextual nets seem to be a better representation for systems exhibiting concurrent read access to shared resources: they can be exponentially smaller than conventional unfoldings on these cases. Theoretical and practical contributions are made. We first study the construction of contextual unfoldings, introducing algorithms and data structures that enable their efficient computation. We integrate contextual unfoldings with merged processes, another representation of concurrent behavior that alleviates the explosion caused by non-determinism. The resulting structure, called contextual merged processes, is often orders of magnitude smaller than unfoldings, as we experimentally demonstrate. Next, we develop verification techniques based on unfoldings. We define SAT encodings for the reachability problem in contextual unfoldings, thus solving the problem of detecting cycles of asymmetric conflict. Also, an unfolding-based decision procedure for fault diagnosis under fairness constraints is presented, in this case only for conventional unfoldings. Finally, we implement our verification algorithms, aiming at producing a competitive model checker intended to handle realistic benchmarks. We subsequently evaluate our methods over a standard set of benchmarks and compare them with existing unfolding-based techniques. The experiments demonstrate that reachability checking based on contextual unfoldings outperforms existing techniques on a wide number of cases. This suggests that contextual unfoldings, and asymmetric event structures in general, have a rightful place in research on concurrency, also from an efficiency point of view.

Les réseaux de Petri et leurs extensions constituent un formalisme très connu pour la modélisation de la spécification des systèmes à évènements discrets temps réel. Pour ces systèmes, les exigences de vérification et de validation sont indispensables pour garantir leur bon fonctionnement car la moindre erreur peut entrainer des conséquences catastrophiques. Pour analyser le comportement du système, il est courant de construire le graphe d’états (ou espace d’états) qui énumère de façon exhaustive les différents états accessibles.Ce graphe permet de vérifier des propriétés génériques comme le caractère borné, l’accessibilité, la terminaison, la vivacité, l’absence de blocage, etc. Mais la construction de cet espace d’états est confrontée au problème d’explosion combinatoire du nombre d’états lié à la complexité et à la concurrence du système.L’une des alternatives pour contenir cette combinatoire est de conserver uniquement les ordres partiels entre les évènements. Le dépliage est une technique d’ordre partiel adaptée à la vérification, au diagnostic et à la planification. Cette thèse contribue à l’étude du dépliage des réseaux de Petri et, plus particulièrement,apporte une contribution au dépliage des réseaux de Petri avec des arcs de reset. De plus, le dépliage explicite les exécutions possibles du système qui sont, par définition, des processus. Il s’agit plus précisément des processus de branchement qui diffèrent des processus classiques. Ainsi, nous proposons une algèbre adaptée aux processus de branchement issus du dépliage des réseaux de Petri. / Petri nets and their extensions are a well-known formalism for modeling the specification of discrete events systems real-time. For these systems, the demands of verification and validation are essential to ensure their smooth functioning because the least error can lead to catastrophic consequences. To analyze the behavior of the system, it is common to construct the stategraph (or state space) which lists exhaustively the different accessible states. This graph allows to check the generic properties such as boundedness, accessibility, termination, vivacity, the absence of blocking, etc. But building this state space is confronted with the problem of combinatorial explosion of the number of states related to the complexity and concurrence of the system. One of the alternatives to contain this combination is to keep only partial orders between events. Unfolding is a partial order adapted to technical verification, diagnosis and planning. This thesis contributes to the study of the unfolding of Petri nets and, in particular, his contributes to the unfolding of Petri nets with reset arcs. Moreover, the unfolding explains the possible executions of the system which are, by definition, the processes. This is specifically the branching processes that differ from conventional processes. Thus, we propose an algebra adapted to the branching process from unfolding of Petri nets.

Les travaux de cette thèse s'inscrivent dans le cadre de la vérification des logiciels et plus particulièrement du test à partir de spécifications algébriques. La soumission d'un jeu de tests exhaustif pour trouver toutes les erreurs d'un programme est généralement impossible. Il faut donc sélectionner un jeu de tests le plus judicieusement possible. Nous avons donc donné une méthode de sélection de tests par dépliage des axiomes de spécifications conditionnelles positives (clauses de Horn pour la logique équationnelle). Celle-ci permet de partitionner le jeu exhaustif des tests. Nous utilisons pour cela un critère de sélection qui utilise les axiomes de la spécification et qui peut être appliqué plusieurs fois de suite. Pour garantir de bonnes propriétés sur ce critère de sélection, nous avons également donné un cadre général pour la normalisation d'arbre de preuve. Il fonctionne pour n'importe quel système formel, et permet d'unifier un grand nombre de résultats en logique.

Le test est l'une des méthodes les plus utilisées pour la validation du logiciel. L'activité de test consiste à exécuter le logiciel sur un sous-ensemble de ses entrées possibles de manière à déceler d'éventuelles erreurs. La présence d'erreurs est établie par confrontation du comportement du logiciel avec un objet de référence. Le processus de test est généralement décomposé en trois phases : la sélection du sous-ensemble des entrées sur lequel le logiciel sera exécuté, la soumission de ces entrées au logiciel en collectant les sorties (les réponses du logiciel) et la décision de l'adéquation de ces sorties avec les sorties attendues.<br /><br />La sélection des données à soumettre au logiciel peut être effectuée selon différentes approches. Lorsque la phase de sélection d'un jeu de tests est opérée à partir d'un objet de référence décrivant plus ou moins formellement le comportement du logiciel, sans connaissance de l'implantation elle-même, on parle de test « boîte noire ». Une des approches de test boîte noire pour laquelle un cadre formel a été proposé est celle qui utilise comme objet de référence une spécification logique du système sous test.<br /><br />Le cadre général de test à partir de spécifications logiques (ou axiomatiques) pose les conditions et les hypothèses sous lesquelles il est possible de tester un système. La première hypothèse consiste à considérer le système sous test comme un modèle formel implantant les opérations dont le comportement est décrit par la spécification. La seconde hypothèse a trait à l'observabilité du système sous test. Il faut fixer la forme des formules qui peuvent être interprétées par le système, c'est-à-dire qui peuvent être des tests. On se restreint généralement au moins aux formules qui ne contiennent pas de variables. Une fois ces hypothèses de test posées, on dispose d'un jeu de tests initial, celui de toutes les formules observables qui sont des conséquences logiques de la spécification. <br /><br />Le premier résultat à établir est l'exhaustivité de cet ensemble, c'est-à-dire sa capacité à prouver la correction du système s'il pouvait être soumis dans son intégralité. Le jeu de tests exhaustif étant le plus souvent infini, une phase de sélection intervient afin de choisir un jeu de tests de taille finie et raisonnable à soumettre au système. Plusieurs approches sont possibles. L'approche suivie dans ma thèse, dite par partition, consiste a diviser le jeu de tests exhaustif initial en sous-jeux de tests, selon un certain critère de sélection relatif à une fonctionnalité ou à une caractéristique du système que l'on veut tester. Une fois cette partition suffisamment fine, il suffit de choisir un cas de test dans chaque sous-jeu de test obtenu en appliquant l'hypothèse d'uniformité (tous les cas de test d'un jeu de test sont équivalents pour faire échouer le système). Le deuxième résultat à établir est que la division du jeu de tests initial n'ajoute pas (correction de la procédure) et ne fait pas perdre (complétude) de cas de test.<br /><br />Dans le cadre des spécifications algébriques, une des méthodes de partition du jeu de tests exhaustif qui a été très étudiée, appelée dépliage des axiomes, consiste à procéder à une analyse par cas de la spécification. Jusqu'à présent, cette méthode s'appuyait sur des spécifications équationnelles dont les axiomes avaient la caractéristique d'être conditionnels positifs (une conjonction d'équations implique une équation).<br /><br />Le travail de ma thèse a eu pour but d'étendre et d'adapter ce cadre de sélection de tests à des systèmes dynamiques spécifiés dans un formalisme axiomatique, la logique modale du premier ordre. La première étape a consisté à généraliser la méthode de sélection définie pour des spécifications équationnelles conditionnelles positives aux spécifications du premier ordre. Ce cadre de test a ensuite été d'adapté à des spécifications modales du premier ordre. Le premier formalisme de spécification considéré est une extension modale de la logique conditionnelle positive pour laquelle le cadre de test a été initialement défini. Une fois le cadre de test adapté aux spécifications modales conditionnelles positives, la généralisation aux spécifications modales du premier ordre a pu être effectuée. <br /><br />Dans chacun de ces formalismes nous avons effectué deux tâches. Nous avons d'une part étudié les conditions nécessaires à imposer à la spécification et au système sous test pour obtenir l'exhaustivité du jeu de tests initial. Nous avons d'autre part adapté et étendu la procédure de sélection par dépliage des axiomes à ces formalismes et montré sa correction et sa complétude. Dans les deux cadres généraux des spécifications du premier ordre et des spécifications modales du premier ordre, nous avons montré que les conditions nécessaires à l'exhausitivité du jeu de test visé étaient mineures car faciles à assurer dans la pratique, ce qui assure une généralisation satisfaisante de la sélection dans ce cadre.

Les ferrures d'ancrage sont des pièces de sécurité automobile qui doivent résister à des chocs éventuels sans se rompre. Elles sont issues de tôles en acier à Haute Limite Elastique et mises en forme par découpage et pliage. L'étude de leur comportement lors de leur fabrication et des qualités mécaniques qui en résulte a été conduite de manière expérimentale et numérique avec confrontation des résultats pour valider la simulation. L'endommagement apporté au matériau est pris en compte dans les routines utilisateur du code EF Abaqus Standard. C'est une des fonctions objectives intervenant dans l'optimisation de la forme des attaches ainsi que dans l'optimisation du procédé de pliage. Les études sont basées sur des plans d'expériences des représentations approchées par surfaces de réponse et la mise en oeuvre d'un réseau de neurones artificiels. Les fonctions objectives sont les efforts exercés sur le poinçon, les contraintes et le dommage lors de l'opération de pliage. Dans les opérations de dépliage figurant le choc dynamique, les fonctions objectives sont l'effort maximal de dépliage, les contraintes et le dommage. La recherche des optima est faite par la méthode des éléments diffus, les stratégies d'évolution et un calcul global. Les paramètres rayon de matrice et jeu entre la tôle et l'outillage sont optimisés en vue de fournir une pièce la plus résistante possible.

Tester la compatibilité cinématique de la géométrie d'une surface de faille (1) et la géométrie d'une écaille qui glisse le long de celte surface de faille (2) est un problème compliqué que nous avons partiellement résolu. Nous avons considéré le problème (1) dans le contexte de blocs rigides et le problème (2) pour une écaille plissée. Nous proposons un critère de moindres carrés permettant de contraindre ia forme des failles de façon compatible avec l'approximation blocs rigides, i.e., les deux" blocs restent en contact et glissent l'un sur l'autre sans déformation. Si celle condition est satisfaite, la surface de faille est un filetage, i.e., une surface qui est partout tangente à un champ de vecteurs (torseur) non nul. Nous contraignons la surface à être le plus près possible des points de données (données de puits ou données sismiques), et régulière (minimisation des courbures principales). Le critère de filetage donne des résultats plus plausibles que la minimisation d'un critère basé seulement sur des dérivées secondes ou sur la matrice de courbure. Il donne aussi une direction de stries. Nous avons testé l'effet de ce critère sur différents exemples naturels (les failles de la Cléry et de San Cayetano). La restauration d'une structure géologique à une époque antérieu!e est un bon moyen de critiquer et d'améliorer l'interprétation de la structure actuelle. Nous nous sommes intéressés au glissement banc sur banc avec conservation des longueurs et du volume. Nous avons déplié un feuilletage par optimisation de différents critères de moindres carrés : horizontalité des isochrones, conservation des longueurs et du volume. Nous avons introduit des contraintes d'égalilé pour traduire la conservation de la reliure (pin-surface). La reliure représente une surface transverse à l'ensemble des feuilles de la structure conservée après dépliage. Nous avons testé notre formulation sur des exemples synthétiques et expérimentaux.

Nous proposons une technique de dépliage pour vérifier les systèmes concurrents infinis bien structurés. Certaines propriétés d'intérêt comme la bornitude, la couverture et la terminaison sont décidables grâce à la bonne structure de ces systèmes. D'autre part, le dépliage réduit efficacement l'explosion combinatoire en exploitant l'ordre partiel entre les événements des systèmes concurrents. Nous proposons une modélisation par structure d'événements pour des systèmes bien structurés élémentaires, tels les compteurs et les files de communication. Le dépliage d'un réseau de structures d'événements étant une structure d'événements, nous proposons ensuite une approche hiérarchique à la modélisation et à la vérification des systèmes, qui préserve la bonne structure. Enfin, nous proposons une technique d'élimination des événements redondants. La mise en œuvre de notre approche dans l'outil ESU nous permet de conclure à son efficacité. / We propose an unfolding technique for verifying concurrent infinite-state systems that are well-structured. Some properties of interest such as boundedness, coverability and termination are decidable thanks to the well-structure of these systems. Moreover, the unfolding effectively reduces the combinatorial explosion by exploiting the partial order between events of concurrent systems. We propose a modelization using event structures for basic well-structured systems, such as counters and communication channels. As the unfolding of a synchronized product of event structures is an event structure, we obtain a hierarchical approach to modeling as well as to verifying systems, which preserves the well-structure. Finally, we propose a technique for eliminating redundant events. The implementation of our approach in the ESU tool allows us to conclude on its efficiency.

Les structures géologiques sont le plus souvent dessinées par interpolations de données dispersées. Un problème est de pouvoir contraindre ces interpolations par des règles géométriques et cinématiques. La méthode dite de l'équilibrage des structures en coupe illustre ce principe. Pour tester la compatibilité de structures à déformation hétérogène, on peut les diviser en éléments dont on considère la déformation comme homogène, mais cette technique est limitée. Une autre méthode, pour s'assurer de la compatibilité géométrique de zones plissées-faillées, consiste à tester la possibilité de restaurer de telles surfaces à leur état initial. Le principe de la méthode est de décrire ces surfaces par des éléments rigides plans et de les rabattre dans le plan horizontal par un programme de calcul (minimisation automatique de vides et de recouvrements). En dépliant différents blocs et en ajustant ces blocs le long de failles, il est possible de retrouver l'état antérieur à la déformation (continue et discontinue). Le programme (UNIX, FORTRAN, station de travail), a été initialement testé sur des exemples théoriques et expérimentaux, puis appliqué à des structures naturelles (gisements pétroliers) avec les applications suivantes: (1) en zone pétrolifère (ou minéralisée), le but est de dessiner au mieux les structures associées aux failles qui peuvent faire office de piège, ce qui permet de mieux contraindre les capacités du gisement et sa géométrie; (2) en l'utilisation plus géodynamique, le champ de déplacement fini associé à la déformation, traduite par les plis et les failles, peut être étudié.