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.

L'adaptation comportementale est primordiale pour faire face à l'environnement flexible dans lequel les individus évoluent chaque Jour, notamment par l'élaboration de comportements d'exploration ou de vérification. Le cortex préfrontal a depuis longtemps été considéré comme le siège du contrôle exécutif nécessaire à la genèse de ces comportements. Deux régions semblent essentielles: le cortex préfrontal latéral (LPFC) et le cortex midcingulaire (MCC). Bien que diverses théories attribuent à ces régions les fonctions d'évaluation des performances et de contrôle cognitif respectivement, leurs rôles dans les comportements de recherche d'information restent imprécis, et cela malgré l'apport potentiel aussi bien dans un contexte normal que pathologique (i.e. troubles obsessionnels compulsifs). Pour mieux comprendre la spécificité de ces régions dans les comportements d’exploration, les travaux que nous avons menés au cours de cette thèse emploient différentes approches comportementales et électrophysiologiques chez les primates humains et non humains. Ils ont permis de (1) raffiner la compréhension de l'implication des régions frontales dans le contrôle cognitif et l'effort attentionnel, (2) développer des tâches comportementales induisant des vérifications, basées sur le Jugement des performances ou l'évaluation de l'environnement, et (3) souligner la spécificité des comportements de vérification. En particulier, nos enregistrements intracérébraux chez le singe en comportement montrent l'importance du MCC pour signaler le besoin d'explorer sur la base de l'évaluation des performances, tandis que le LPFC contribue à la mise en oeuvre de la conduite comportementale à adopter / Behavioural adaptation is an essential element of our quest to survive and flourish in a volatile environment, in particular by the use of exploration and verification behaviours. The prefrontal cortex has long been considered a critical source of these behaviours given it role in executive control. Two regions appear to be particularly critical – the lateral prefrontal cortex (LPFC), and the midcingulate cortex (MCC). Although numerous theories associate these regions with the functions of performance evaluation and cognitive control, the role of these regions in the search for information remains lacking, despite the importance of these behaviours and their apparent role in pathologies such as obsessive compulsive disorders. This thesis seeks to understand the specific roles of these regions in exploratory behaviours, employing a range of behavioural and electrophysiological techniques in both human and non human primates. The work here helps to refine our understanding of the role of frontal cortical regions in cognitive control and attentional effort. Moreover, we have developed a number of behavioural tasks that induce verification behavior based on subjects’ evaluation of their own performance or on an evaluation of the environment. Our work reveals the specificity of verification behaviour as well as specific roles for the MCC and LPFC in this search for information. Our intra cerebral recordings in monkeys working on such tasks underline the importance of the MCC for signalling the need to explore the environment on the basis of performance evaluation, whilst we have also shown the role of LPFC in the implementation of the necessary behavioural adaptations

Les équipements intelligents, notamment les smartphones, sont la cible de nombreuses attaques de sécurité. Par ailleurs, la mise en œuvre de mécanismes de protection usuels est souvent inadaptée du fait de leurs ressources fortement contraintes. Dans ce contexte, nous proposons d'utiliser des chaînes de fonctions de sécurité qui sont composées de plusieurs services de sécurité, tels que des pare-feux ou des antivirus, automatiquement configurés et déployés dans le réseau. Cependant, ces chaînes sont connues pour être difficiles à valider. Cette difficulté est causée par la complexité de ces compositions qui impliquent des centaines, voire des milliers de règles de configuration. Dans cette thèse, nous proposons l'architecture d'un orchestrateur exploitant la programmabilité des réseaux pour automatiser la configuration et le déploiement de chaînes de fonctions de sécurité. Il est important que ces chaînes de sécurité soient correctes afin d’éviter l'introduction de failles de sécurité dans le réseau. Aussi, notre orchestrateur repose sur des méthodes automatiques de vérification et de synthèse, encore appelées méthodes formelles, pour assurer la correction des chaînes. Notre travail appréhende également l'optimisation du déploiement des chaînes dans le réseau, afin de préserver ses ressources et sa qualité de service. / Smart environments, in particular smartphones, are the target of multiple security attacks. Moreover, the deployment of traditional security mechanisms is often inadequate due to their highly constrained resources. In that context, we propose to use chains of security functions which are composed of several security services, such as firewalls or antivirus, automatically configured and deployed in the network. Chains of security functions are known as being error prone and hard to validate. This difficulty is caused by the complexity of these constructs that involve hundreds and even thousands of configuration rules. In this PhD thesis, we propose the architecture of an orchestrator, exploiting the programmability brought by software defined networking, for the automated configuration and deployment of chains of security functions. It is important to automatically insure that these security chains are correct, before their deployment in order to avoid the introduction of security breaches in the network. To do so, our orchestrator relies on methods of automated verification and synthesis, also known as formal methods, to ensure the correctness of the chains. Our work also consider the optimization of the deployment of chains of security functions in the network, in order to maintain its resources and quality of service.

La préservation de propriétés établies sur le programme source jusqu'au code exécutable est un point important dans les méthodes formelles. Cette propriété de préservation est établie par la vérification formelle du proccessus de compilation. Un compilateur est formellement vérifié s'il est accompagné d'une preuve de préservation sémantique : "si la compilation réussit, le code compilé se comporte comme le code source le prédit." Le projet CompCert étudie la vérification formelle de compilateurs réalistes utilisable dans l'embarqué-critique. Il s'agit de développer et formellement vérifier de tels compilateur via l'assistant de preuve Coq. Un compilateur pour le langage C vers l'assembleur PowerPC a déjà ainsi été produit. Le code exécutable du compilateur a été obtenu en deux étapes non vérifiés : la génération automatique de code Ocaml par le mécanisme d'extration de Coq et la compilation du de ce code extrait par le système Objective Caml. En fait, cette lacune est commune à tous les développements spécifiés dans l'assistant de preuve Coq et destinés à produire un éxécutable. Cette thèse décrit l'étude, le développement et la vérification formelle, dans l'assistant de preuve Coq, d'un compilateur pour le fragment purement fonctionnel du langage ML : le langage cible du mécanisme d'extraction de Coq. Concrètement, il s'git d'une chaîne de compilation en amont pour mini-ML (lambda calcul, let, letrec et filtrage) vers le premier langage intermédiaire de la chaîne de compilation en aval du compilateur CompCert. Ce langage, Cminor, est un langage de bas niveau à la C. L'expressivité du langage source traité rend ce compilateur réaliste. Il comporte aussi des optimisations classiques propre à la compilation de langages fonctionnels : la décurryfication, comme celle implémentée dans le compilateur OCaml ; la représentation uniforme des données, explicitation des fermetures, numérotation des constructeurs et une mise en style par passage de continuation (CPS) optimisée. Le point fort de ce compilateur et que, comme les compilateurs modernes pour langage de haut niveau, il peut interagir avec un gestionnaire de mémoire automatique. Cette interaction a aussi été formellement vérifiée.

L'utilisation omniprésente des systèmes informatiques impose de s'assurer de leur bon fonctionnement. Dans ce but, les méthodes de vérification formelle permettent de suppléer les simulations qui ne peuvent être complètement exhaustives du fait de la complexité croissante des systèmes. Le model checking fait partie de ces méthodes et présente l'avantage d'être complètement automatisée. Cette méthode consiste à développer des algorithmes pour vérifier qu'une spécification exprimée la plupart du temps sous la forme d'une formule logique est satisfaite par un modèle du système. Les langages historiques de spécification utilisent comme formules atomiques des variables propositionnelles qui permettent d'exprimer principalement des propriétés portant sur les états de contrôle du modèle. Le but de cette thèse est de vérifier des propriétés plus riches portant sur diverses données manipulées par les modèles: des compteurs, des horloges ou des queues. Ces données peuvent prendre une infinité de valeurs et induisent donc des modèles avec un nombre infini d'états. Nous définissons un cadre général pour l'extension des logiques temporelles avec des contraintes permettant de comparer la valeur des variables a différents états de l'exécution. Nous établissons des résultats de décidabilité et complexité pour des problèmes de model checking impliquant diverses instances de ces extensions. Nous privilégions pour cela l'approche à base d'automates en combinant des constructions connues pour les logiques propositionnelles classiques avec des méthodes d'abstraction des modèles dont les variables sont interprétées dans des domaines infinis.

L'étude de cette thèse porte sur trois méthodes de validation dynamiques : les méthodes de vérification, d'enforcement (mise en application), et de test de propriétés lors de l'exécution des systèmes. Nous nous intéresserons à ces approches en l'absence de spécification comportementale du système à valider. Pour notre étude, nous nous plaçons dans la classification Safety-Progress des propriétés. Ce cadre offre plusieurs avantages pour la spécification de propriétés sur les systèmes. Nous avons adapté les résultats de cette classification, initialement développés pour les séquences infinies, pour prendre en compte de manière uniforme les séquences finies. Ces dernières peuvent être vues comme une représentation abstraite de l'exécution d'un système. Se basant sur ce cadre général, nous nous sommes intéressés à l'applicabilité des méthodes de validation dynamiques. Nous avons caractérisé les classes de propriétés vérifiables, enforçables, et testables. Nous avons ensuite proposé trois approches génériques de vérification, d'enforcement, et de test de propriétés opérant à l'exécution des systèmes. Nous avons montré comment il était possible d'obtenir, à partir d'une propriété exprimée dans le cadre de la classification Safety-Progress, des mécanismes de vérification, d'enforcement, ou de test dédiés à la propriété considérée. Enfin, nous proposons également les outils j-VETO et j-POST mettant en œuvre l'ensemble des résultats proposés sur les programmes Java.

La fiabilité des logiciels est un facteur critique de notre société~: toute panne, tout bogue, tout dysfonctionnement, perturbe la bonne marche de nos activités avec parfois des conséquences humaines, financières ou morales importantes. Contrairement à d'autres domaines industriels plus anciens, la démarche qualité en informatique n'en est encore qu'à ses débuts. Il est couramment convenu comme normal qu'un ordinateur perde un fichier ou que l'installation d'un nouveau logiciel en rende un autre inutilisable. Cependant, dans des domaines précis (banque, systèmes embarqués, médecine, etc.), dits critiques, on ne peut se permettre d'avoir un système défaillant~: une phase importante du développement logiciel est celle de la validation durant laquelle le système est analysé afin de garantir qu'il respecte certaines exigences de fiabilité. Cette phase de validation fait appel à deux approches complémentaires, le test et la vérification. Les travaux présentés dans cette habilitation concernent majoritairement la verification par la technique dite de "model-checking". Une première partie montre des techniques originales pour la vérification de protocoles de sécurité. D'autres travaux, plus théoriques, portent sur l'accélération de relations de semi-commutation ainsi que sur la vérification de propriétés non fonctionnelles. Enfin, des résultats sur la génération aléatoire de structures complexes sont développés dans le contexte du test à partir de modèles et du test de performances.

Nous nous intéressons dans ce document à la génération automatique de tests de conformité pour des implémentations réactives. Nous nous attachons dans un premier temps à étendre la méthode de génération de tests, basée sur la théorie du test de conformité à la ioco, en reliant trois niveaux de description (propriétés, spécification et implémentation). Nous combinons pour cela vérification formelle et test de conformité. Nous obtenons ainsi, lors de l'exécution du cas de test sur l'implémentation, des verdicts pouvant indiquer la non-conformité de l'implémentation, mais également la satisfaction/violation de la propriété par l'implémentation et/ou la spécification. Nous étendons dans un deuxième temps la génération de tests par l'expressivité du modèle de spécification en nous intéressant aux spécifications interprocédurales récursives. Notre méthode est basée sur une analyse exacte de co-accessibilité permettant de décider si et comment un objectif de test pourra être atteint. Cependant, l'incapacité des cas de test récursifs à connaître leur propre pile d'exécution ne permet pas d'utiliser la totalité des résultats de l'analyse. Nous discutons de ce problème d'observation partielle et de ses conséquences puis nous proposons un moyen de minimiser son impact. Enfin, nous expérimentons ces méthodes de génération de tests sur quelques exemples et une étude de cas

Nous proposons dans cette thèse une démarche permettant de décrire un DSML (Domain Specific Modeling Language) et les outils nécessaires à l'exécution, la vérification et la validation des modèles. La démarche que nous proposons offre une architecture générique de la syntaxe abstraite du DSML pour capturer les informations nécessaires à l'exécution d'un modèle et définir les propriétés temporelles qui doivent être vérifiées. Nous nous appuyons sur cette architecture pour expliciter la sémantique de référence et l'implanter. Plus particulièrement, nous étudions les moyens :<br />- d'exprimer et de valider la définition d'une traduction vers un domaine formel dans le but de réutiliser des outils de model-checking.<br />- de compléter la syntaxe abstraite par le comportement; et profiter d'outils génériques pour pouvoir simuler les modèles construits.<br />Enfin, de manière à valider les différentes sémantiques implantées vis-à-vis de la sémantique de référence, nous proposons un cadre formel de métamodélisation.

Cette thèse propose une Démarche de Vérification Formelle d'Architectures Logicielles : DVFAL. La démarche DVFAL supporte divers formalismes de description d'architectures logicielles tels que : les ADL (langages de description d'architectures), UML2.0, Symphony et des profils UML2.0 dédiés au domaine des architectures logicielles. La démarche DVFAL préconise l'ADL Wright en tant que langage formel pivot permettant de représenter des architectures logicielles décrites dans les divers formalismes. En outre, elle propose des transformations de modèles sous forme des traducteurs (Wright vers CSP de Hoare et Wright vers Ada) pour bénéficier des outils de vérification des propriétés supportant CSP et Ada tels que FDR et FLAVERS. Enfin, la démarche DVFAL propose un profil UML2.0-Wright jouant le rôle d'un langage intermédiaire entre les formalismes à base d'UML et Wright.