Cette thèse se situe au croisement de deux domaines : la sûreté de fonctionnement des systèmes critiques et les méthodes formelles. Nous cherchons à établir la cohérence des analyses de sûreté de fonctionnement réalisées à l’aide de modèles représentant un même système à des niveaux de détail différents. Pour cela, nous proposons une notion de raffinement dans le cadre de la conception de modèles AltaRica : un modèle détaillé raffine un modèle abstrait si le modèle abstrait simule le modèle détaillé. La vérification du raffinement de modèles AltaRica est supportée par l’outil de model-checking MecV. Ceci permet de réaliser des analyses multi-systèmes à l’aide de modèles à des niveaux de détail hétérogènes : le système au centre de l’étude est détaillé tandis que les systèmes en interface sont abstraits. Cette approche a été appliquée à l’étude d’un système de contrôle de gouverne de direction d’un avion connecté à un système de génération et distribution électrique. / This thesis links two fields : system safety analyses and formal methods.We aim at checking the consistensy of safety analyses based on formal models that represent a system at different levels of detail. To reach this objective, we introduce a refinement notion in the AltaRica modelling process : a detailed model refines an abstract model if the abstract model simulates the detailed model. The AltaRica model refinement verification is supported by the MecV model-checker. This allows to perform multi-system safety analyses using models with heterogeneous levels of detail : the main system is detailed whereas the interfaced systems remain abstract. This approach has been applied to the analysis of a rudder control system linked to an electrical power generation and distribution system.

Le Cloud Computing est de plus en plus utilisé pour le déploiement et l'exécution des applications métiers et plus particulièrement des applications à base de services (AbSs). L'élasticité à différents niveaux est l'une des propriétés fournies par le Cloud. Son principe est de garantir la fourniture des ressources nécessaires et suffisantes pour la continuité de l'exécution optimale des services Cloud. La fourniture des ressources doit considérer la variation de la demande pour éviter la sous-utilisation et la surutilisation de ces dernières. Il est évident que la fourniture d'infrastructures et/ou de plateformes élastiques n'est pas suffisante pour assurer l'élasticité des applications métiers déployées. En effet, il est aussi nécessaire de considérer l'élasticité au niveau des applications. Ceci permet l'adaptation dynamique des applications déployées selon la variation des demandes. Par conséquent, les applications métiers doivent être fournies avec des mécanismes d'élasticité permettant leur adaptation tout en assurant les propriétés fonctionnelles et non-fonctionnelles désirées. Dans nos travaux, nous nous sommes intéressés à la fourniture d'une approche holistique pour la modélisation, l'évaluation et la mise en oeuvre des mécanismes d'élasticité des AbSs dans le Cloud. En premier lieu, nous avons proposé un modèle formel pour l'élasticité des AbSs. Pour cela, nous avons modélisé les AbSs en utilisant les réseaux de Petri et défini deux opérations d'élasticité (la duplication et la consolidation). En outre, nous avons proposé de coupler ces deux opérations avec un contrôleur d'élasticité. Pour assurer l'élasticité des AbSs, le contrôleur analyse l'exécution des AbSs et prend des décisions sur les opérations d'élasticité (duplication/consolidation). Après la définition de notre modèle pour l'élasticité des AbSs, nous nous sommes intéressés à l'évaluation de l'élasticité avant de l'implémenter dans des environnements Cloud réels. Pour cela, nous avons proposé d'utiliser notre contrôleur d'élasticité comme un Framework pour la validation et l'évaluation de l'élasticité en utilisant des techniques de vérification et de simulation. Enfin, nous avons mis en oeuvre l'élasticité des AbSs dans des environnements Cloud réels. Pour cela, nous avons proposé deux approches. La première approche encapsule les AbSs non-élastiques dans des micro-conteneurs, étendus avec nos mécanismes d'élasticité, avant de les déployer sur des infrastructures Cloud. La seconde approche intègre notre contrôleur d'élasticité dans une infrastructure autonomique afin de permettre l'ajout dynamique des fonctionnalités d'élasticité aux AbSs déployées sur des plateformes Cloud / Cloud computing is being increasingly used for deploying and executing business processes and particularly Service-based Business Processes (SBPs). Among other properties, Cloud environments provide elasticity at different scopes. The principle of elasticity is to ensure the provisioning of necessary and sufficient resources such that a Cloud service continues running smoothly even when the number or quantity of its utilization scales up or down, thereby avoiding under-utilization and over-utilization of resources. It is obvious that provisioning of elastic infrastructures and/or platforms is not sufficient to provide elasticity of deployed business processes. In fact, it is also necessary to consider the elasticity at the application scope. This allows the adaptation of deployed applications during their execution according to demands variation. Therefore, business processes should be provided with elasticity mechanisms allowing their adaptation to the workload changes while ensuring the desired functional and non-functional properties. In our work, we were interested in providing a holistic approach for modeling, evaluating and provisioning of elastic SBPs in the Cloud. We started by proposing a formal model for SBPs elasticity. To do this, we modeled SBPs using Petri nets and defined two elasticity operations (duplication / consolidation). In addition, we proposed to intertwine these elasticity operations with an elasticity controller that monitors SBPs execution, analyzes monitoring information and executes the appropriate elasticity operation (duplication/consolidation) in order to enforce the elasticity of SBPs. After facing the challenge of defining a model and mechanisms for SBPs elasticity, we were interested in the evaluation of elasticity before implementing it in real environments. To this end, we proposed to use our elasticity controller as a framework for the validation and evaluation of elasticity using verification and simulation techniques. Finally, we were interested in the provisioning of elasticity mechanisms for SBPs in real Cloud environments. For this aim, we proposed two approaches. The first approach packages non-elastic SBPs in micro-containers, extended with our elasticity mechanisms, before deploying them in Cloud infrastructures. The second approach integrates our elasticity controller in an autonomic infrastructure to dynamically add elasticity facilities to SBPs deployed on Cloud platforms

Ce mémoire présente plusieurs définitions de sémantiques formelles et de transformations de programmes, et expose les choix de conception associés. En particulier, ce mémoire décrit une transformation de programmes inspirée de l'évaluation partielle et dédiée à la compréhension de programmes scientifiques écrits en Fortran. Il détaille également le front-end d'un compilateur réaliste du langage C, ayant été formellement vérifié en C.

Certains problèmes nécessitent des performances que seules les machines massivement parallèles<br />ou les méta-ordinateurs peuvent offrir. L'écriture d'algorithmes pour ce type de machines demeure<br />plus difficile que pour celles strictement séquentielles et la conception de langages adaptés est un sujet de<br />recherche actif nonobstant la fréquente utilisation de la programmation concurrente. En effet, la conception<br />d'un langage de programmation est le résultat d'un compromis qui détermine l'équilibre entre les différentes<br />qualités du langage telles que l'expressivité, la sûreté, la prédiction des performances, l'efficacité ou<br />bien la simplicité de la sémantique.<br />Dans des travaux antérieurs à cette thèse, il a été entrepris d'approfondir la position intermédiaire que le<br />paradigme des patrons occupe. Toutefois il ne s'agissait pas de concevoir un ensemble a priori fixé d'opérations<br />puis de concevoir des méthodologies pour la prédiction des performances, mais de fixer un modèle<br />de parallélisme structuré (avec son modèle de coûts) puis de concevoir un ensemble universel d'opérations<br />permettant de programmer n'importe quel algorithme de ce modèle. L'objectif est donc le suivant : parvenir<br />à la conception de langages universels dans lesquels le programmeur peut se faire une idée du coût à partir<br />du code source.<br />Cette thèse s'inscrit dans le cadre du projet «CoordinAtion et Répartition des Applications Multiprocesseurs<br />en objective camL» (CARAML) de l'ACI GRID dont l'objectif était le développement de bibliothèques<br />pour le calcul haute-performance et globalisé autour du langage OCaml. Ce projet était organisé en trois<br />phases successives : sûreté et opérations data-parallèles irrégulières mono-utilisateur ; opérations de multitraitement<br />data-parallèle ; opérations globalisées pour la programmation de grilles de calcul.<br />Ce tapuscrit est organisé en 3 parties correspondant chacune aux contributions de l'auteur dans chacune<br />des phases du projet CARAML : une étude sémantique d'un langage fonctionnel pour la programmationBSP<br />et la certification des programmes écrits dans ce langage ; une présentation d'une primitive de composition<br />parallèle (et qui permet aussi la programmation d'algorithmes «diviser-pour-régner» parallèles), un exemple<br />d'application via l'utilisation et l'implantation de structures de données parallèles et une extension pour les<br />entrées/sorties parallèles en BSML ; l'adaption du langage pour le méta-calcul.

Nous étudions la modélisation et la validation hors-ligne des applications temps-réel en environnement monoprocesseur, qui prend explicitement en compte l'échange des messages, le partage des ressources et les instructions conditionnelles entre les tâches. Notre objectif est de mettre en évidence l'impact de ces paramètres sur l'analyse des applications. Classiquement, ces applications sont modélisées de façon linéaire, en encapsulant les blocs conditionnels, et les séquences sont utilisées pour leur validation. Nous proposons une approche de modélisation et de validation arborescente, qui permet de considérer de façon explicite les blocs conditionnels, et qui utilise les arbres d'ordonnancement pour la validation. Nous comparons ensuite ces deux approches, et prouvons que les premières sont parfois trop pessimistes, c'est à dire qu'elles peuvent conduire à déclarer certaines applications comme non ordonnançables, alors qu'en réalité elles le sont. Nous commençons par construire un générateur d'arbres d'ordonnancement valides. La complexité du générateur étant exponentielle en fonction du nombre de tâches, cette approche est di cile à mettre en ÷uvre dans la pratique. Nous proposons donc une approche de modélisation bas ée sur les réseaux de Petri. Ce réseau sera utilisé pour générer les arbres valides, par construction du graphe de marquages, et la complexité pourra être réduite grâce à des heuristiques.

Les systèmes multi-agents (SMA) peuvent être utilisé pour modéliser les phénomènes qui peuvent être décomposés en plusieurs agents qui interagissent et qui existent au sein d'un environnement. En particulier, ils peuvent être utilisés pour modéliser les sociétés humaines et animales, aux fins de l'analyse de leurs propriétés par des moyens de calcul. Cette thèse est consacrée à l'analyse automatisée d'un type particulier de ces modèles sociaux, à savoir, celles qui sont fondées sur les principes comportementalistes, qui contrastent avec les approches cognitives plus dominante dans la littérature des SMAs. La caractéristique des théories comportementalistes est l'accent mis sur la définition des comportements basée sur l'interaction entre les agents et leur environnement. De cette manière, non seulement des actions réflexives, mais aussi d'apprentissage, les motivations, et les émotions peuvent être définies. Plus précisément, dans cette thèse, nous introduisons une architecture formelle d'agent (spécifiée avec la Notation Z) basée sur la théorie d'analyse comportementale de B. F. Skinner, ainsi que une notion appropriée et formelle de l'environnement (basée sur l'algèbre de processus pi-calculus) pour mettre ces agents ensemble dans un SMA. La simulation est souvent utilisée pour analyser les SMAs. Les techniques consistent généralement à simuler le SMA plusieurs fois, soit pour recueillir des statistiques, soit pour voir ce qui se passe à travers l'animation. Toutefois, les simulations peuvent être utilisés d'une manière plus orientée vers la vérification si on considère qu'elles sont en réalité des explorations de grandes espaces d'états. Dans cette thèse nous proposons une technique de vérification nouvelle basé sur cette idée, qui consiste à simuler un SMA de manière guidée, afin de vérifier si quelques hypothèses sur lui sont confirmées ou non. À cette fin, nous tirons profit de la position privilégiée que les environnements sont dans les SMAs de cette thèse: la spécification formelle de l'environnement d'un SMA sert à calculer les évolutions possibles du SMA comme un système de transition, établissant ainsi l'espace d'états à vérifier. Dans ce calcul, les agents sont pris en compte en les simulant afin de déterminer, à chaque état de l'environnement, quelles sont leurs actions. Chaque exécution de la simulation est une séquence d'états dans cet espace d'états, qui est calculée à la volée, au fur et à mesure que la simulation progresse. L'hypothèse à étudier, à son tour, est donnée comme un autre système de transition, appelé objectif de simulation, qui définit les simulations désirables et indésirables (e.g., "chaque fois que l'agent fait X, il fera Y plus tard"). Il est alors possible de vérifier si le SMA est conforme à l'objectif de simulation selon un certain nombre de notions de satisfiabilité très précises. Algorithmiquement, cela correspond à la construction d'un produit synchrone de ces deux systèmes de transitions (i.e., celui du SMA et l'objectif de simulation) à la volée et à l'utiliser pour faire fonctionner un simulateur. C'est-à-dire, l'objectif de simulation est utilisé pour guider le simulateur, de sorte que seuls les états concernés sont en réalité simulés. À la fin d'un tel algorithme, il délivre un verdict concluant ou non concluant. Si c'est concluant, il est connu que le SMA est conforme à l'objectif de simulation par rapport aux observations qui ont été faites lors des simulations. Si c'est non-concluant, il est possible d'effectuer quelques ajustements et essayer à nouveau. En résumé, donc, dans cette thèse nous fournissons quatre nouveaux éléments: (i) une architecture d'agent; (ii) une spécification formelle de l'environnement de ces agents, afin qu'ils puissent être composés comme un SMA; (iii) une structure pour décrire les propriétés d'intérêt, que nous avons nommée objectif de simulation, et (iv) une technique pour l'analyse formelle du SMA résultant par rapport à un objectif de simulation. Ces éléments sont mis en œuvre dans un outil, appelé Simulateur Formellement Guidé (FGS, de l'anglais Formally Guided Simulator). Des études de cas exécutables dans FGS sont fournies pour illustrer l'approche.

Le but de ce rapport est de présenter une méthode globale de développement à partir de spécifications informelles, depuis la modélisation graphique des exigences temporelles d'un système ferroviaire critique jusqu'à une implantation systématique au moyen de méthodes formelles. Nous proposons d'utiliser ici les réseaux de Petri temporels pour décrire le comportement attendu du logiciel de contrôle-commande à construire.Tout d'abord nous construisons un modèle des exigences p-temporel prenant en compte toutes les contraintes que doit vérifier le système. Nous proposons des outils et des méthodes capables de valider et de vérifier ce modèle. Ensuite, il s'agit de construire un modèle de processus solution en réseau de Petri t-temporel. Ce modèle illustre des exigences techniques relatives à un choix technologique ou architectural. L'objectif est double : tout d'abord il est nécessaire de vérifier la traçabilité des exigences ; ensuite, il faut vérifier que l'ensemble des exigences sources sont bien implémentées dans la solution préconisée et dans sa mise en oeuvre. Enfin, nous proposons une approche visant à transformer de façon systématique le modèle de processus en machine abstraite $B$ afin de poursuivre une procédure formelle $B$ classique. Finalement, le cas d'étude du passage à niveau, composant critique dans le domaine de la sécurité ferroviaire est décrit

Dans le cadre de son offre de serveurs haut de gamme, la société Bull conçoit des multiprocesseurs à mémoire distribuée partagée avec un protocole de cohérence de cache CC-DSM (Cache-Coherent Distibuted Shared Memory), et fournit une implémentation de la bibliothèque MPI (Message Passing Interface) pour la programmation parallèle. L'évaluation des performances de cette implémentation permettra, d'une part, de faire les bons choix d'architecture matérielle et de la couche logicielle au moment de la conception et, d'autre part, fournira des éléments d'analyse nécessaires pour comprendre les mesures faites au moment de la validation de la machine réelle. Nous proposons et mettons en œuvre dans ce travail de thèse une méthodologie permettant d'évaluer les performances des algorithmes de la bibliothèque MPI (ping-pong et barrières) en tenant compte de l'architecture matérielle. Cette approche est basée sur l'utilisation des méthodes formelles, elle consiste en 3 étapes principales : 1) la modélisation en langage LOTOS des aspects matériels (topologie d'interconnexion et protocole de cohérence de cache) et logiciels (algorithmes MPI) ; 2) la vérification formelle de la correction fonctionnelle du modèle obtenu ; 3) l'évaluation des performances après l'extension du modèle par des informations quantitatives (latences des transferts des données) en utilisant des méthodes numériques et de la simulation.

Les séquences de jeux sont une méthodologie établie pour structurer les preuves cryptographiques. De telles preuves peuvent être formalisées rigoureusement en regardant les jeux comme des programmes probabilistes et en utilisant des méthodes de vérification de programmes. Cette thèse décrit CertiCrypt, un outil permettant la construction et vérification automatique de preuves basées sur les jeux. CertiCrypt est implémenté dans l'assistant à la preuve Coq, et repose sur de nombreux domaines, en particulier les probabilités, la complexité, l'algèbre, et la sémantique des langages de programmation. CertiCrypt fournit des outils certifiés pour raisonner sur l'équivalence de programmes probabilistes, en particulier une logique de Hoare relationnelle, une théorie équationnelle pour l'équivalence observationnelle, une bibliothèque de transformations de programme, et des techniques propres aux preuves cryptographiques, permettant de raisonner sur les évènements. Nous validons l'outil en formalisant les preuves de sécurité de plusieurs exemples emblématiques, notamment le schéma de chiffrement OAEP et le schéma de signature FDH.

Le travail coopératif est un domaine qui étudie le travail de groupes d'utilisateurs de façon générale. Sa finalité est la conception de collecticiels, ensembles logiciels qui contiennent les outils, les applications, et les plate-formes qui supportent les activités de groupes d'utilisateurs. La gestion de ces groupes et les échanges d'information entre leurs membres nécessitent la définition de nouveaux services de communication adaptés aux besoins des agents en coopération. Les travaux menés dans ce mémoire ont consisté à définir, à concevoir et à gérer la structuration des groupes coopératifs. Un modèle à base de graphes a été proposé à partir du partage de données, pour représenter les relations entre les divers membres d'un groupe coopératif. A partir de ce modèle, un service pour l'entrée et la sortie en coopération des agents coopérants a été défini. Un protocole de communication sous-jacent a été spécifié en utilisant le langage de description formelle Estelle. Le protocole proposé a été vérifié en utilisant l'environnement à base de réseaux de Petri VAL, puis a été implanté en langage C sous UNIX à partir du code Estelle généré. Une extension de ce travail permet la formation d'apartés qui sont des sous-groupes très dynamiques créés à l'intérieur de la coopération. Un autre protocole spécifié en Estelle a été proposé pour gérer la formation de ces apartés et leur évolution au sein de la coopération. En plus de la structuration des groupes, une étude des données qui peuvent être échangées entre des agents coopérants a mené à la définition d'un service de gestion des dépendances de données. Ce service, spécifié également en Estelle, permet de créer, supprimer ou modifier des dépendances entre données, et répercute les modifications de valeurs vers l'ensemble des données dépendantes.