Tesis sobre el tema "Safety logiciel"

La vérification et la validation de systèmes critiques temps réel sont des activités soumises à de contraignants standards et certifications. Les progrès récents en Ingénierie Système basée sur les modèles peuvent être appliqués en utilisant des techniques formelles de vérification dès la phase amont avec un grand bénéfice pour détecter des défauts. Cette thèse propose une méthodologie basée sur les modèles dédiée à la validation fonctionnelle de tels systèmes. La méthode est dirigée par la couverture structurelle du modèle en Lustre d’un système réactif en co-simulation avec un procédé physique et aussi par les besoins fonctionnels. La méthode s’appuie sur l’utilisation répétitive d’un model-checker et permet de générer des séquences en boucle ouverte. Nous proposons aussi un raffinement qui supporte le passage de cette séquence de tests aux cas de tests en boucle fermée. Nous prenons en compte le problème de l’explosion combinatoire de model-checking. Et finalement nous proposons une heuristique dite vérification hybride combinant model-checking et simulation
The verification and validation of safety-critical real-time system are subject to stringent standards and certifications. Recent progress in model-based system engineering should be applied to such systems since it allows early detection of defects and formal verification techniques. This thesis proposes a model-based testing (MBT) methodology dedicated to functional validation of safety-critical real-time systems. The method is directed by the structural coverage of the Lustre model co-simulated with tje physical process and also by the functional requirements. It relies on a repetitive use of a model checker to generate coverage-based open-loop test sequences. We also propose a refinement technique of progressively adding environment constraints during test generation. The refinement is expected to support the passage from coverage-based open-loop test sequence to functional requirements-based closed-loop test case. Our methodology also considers the state explosion problem of a model checker and proposes a heuristic called hybrid verification combining model checking and simulation

Dans le cadre de l'utilisation de la méthode formelle B, nous proposons de contribuer à l'évaluation des développements de logiciels critiques, par la mise en place de techniques quantitatives. Ces techniques s'articulent autour de la définition, de l'extraction et de l'interprétation de mesures (ou métriques) issues du produit à évaluer. Notre progression vers cet objectif se décompose en trois étapes. La première étape est constituée par la modélisation des spécifications formelles définissant le logiciel. Le modèle obtenu repose sur l'ensemble des arbres syntaxiques correspondant à chaque composant B. Ces arbres sont obtenus par la définition d'une grammaire BNF (backus-naur form) couvrant l'intégralité de la notation B. Ceci nous a amené à proposer des modifications de la notation B. La deuxième étape consiste à définir des mesures primitives à partir des informations contenues dans les arbres syntaxiques des composants B. Ces mesures sont basées sur un mécanisme générique de filtrage syntaxique arborescent. La troisième étape concerne la définition de mesures spécifiques adaptées aux caractéristiques de la méthode B. Nous donnons trois exemples de mesures spécifiques. La première mesure, LARA, concerne l'évaluation de la phase de preuve, la deuxième mesure, MONA, évalue le niveau d'abstraction des spécifications formelles et enfin la troisième mesure, CIEL, s'efforce de caractériser la complexité des spécifications formelles. Pour terminer, sur une étude de cas bien connue, la chaudière (Boiler), nous appliquons les outils développés pour extraire ces mesures. Nous présentons les valeurs obtenues sous une forme graphique spécialement adaptée à la structure des projets B, et nous montrons comment ces outils peuvent-être utilisés pour élaborer des analyses portant sur la qualité globale des développements de logiciel en B.

Les chercheurs dans le domaine de la conception aérodynamique et de la fabrication des avions ont fait beaucoup d'effort pour améliorer les performances des ailes par des techniques d'optimisation. Le développement de la mécanique des fluides numérique a permis de réduire les dépenses en soufflerie tout en fournissant des résultats convaincants pour simuler des situations compliquées des aéronefs. Dans cette thèse, il a été choisi une partie spéciale et importante de l'avion, à savoir, la structure de l'aile. L'optimisation basée sur la fiabilité est une méthode plus appropriée pour les structures sous incertitudes. Il se bat pour obtenir le meilleur compromis entre le coût et la sécurité tout en tenant compte des incertitudes du système en intégrant des mesures de fiabilité au sein de l'optimisation. Malgré les avantages de l'optimisation de la fiabilité en fonction, son application à un problème d'ingénierie pratique est encore assez difficile. Dans notre travail, l'analyse de l'incertitude dans la simulation numérique est introduite et exprimée par la théorie des probabilités. La simulation de Monte Carlo comme une méthode efficace pour propager les incertitudes dans le modèle d'éléments finis de la structure est ici appliquée pour simuler les situations compliquées qui peuvent se produire. Pour améliorer l'efficacité de la simulation Monte Carlo dans le processus d'échantillonnage, la méthode de l'Hypercube Latin est effectuée. Cependant, l'énorme base de données de l'échantillonnage rend difficile le fait de fournir une évaluation explicite de la fiabilité. L'expansion polynôme du chaos est présentée et discutée. Le modèle de Kriging comme un modèle de substitution joue un rôle important dans l'analyse de la fiabilité. Les méthodes traditionnelles d'optimisation ont des inconvénients à cause du temps de calcul trop long ou de tomber dans un minimum local causant une convergence prématurée. Le recuit simulé est une méthode heuristique basée sur une recherche locale, les Algorithmes Génétiques puisent leur inspiration dans les principes et les mécanismes de la sélection naturelle, qui nous rendent capables d'échapper aux pièges des optimums locaux. Dans l'optimisation de la conception de base de la fiabilité, ces deux méthodes ont été mises en place comme procédure d'optimisation. La boucle de l'analyse de fiabilité est testée sur le modèle de substitution
Tremendous struggles of researchers in the field of aerodynamic design and aircraft production were made to improve wing airfoil by optimization techniques. The development of computational fluid dynamic (CFD) in computer simulation cuts the expense of aerodynamic experiment while provides convincing results to simulate complicated situation of aircraft. In our work, we chose a special and important part of aircraft, namely, the structure of wing.Reliability based optimization is one of the most appropriate methods for structural design under uncertainties. It struggles to seek for the best compromise between cost and safety while considering system uncertainties by incorporating reliability measures within the optimization. Despite the advantages of reliability based optimization, its application to practical engineering problem is still quite challenging. In our work, uncertainty analysis in numerical simulation is introduced and expressed by probability theory. Monte Carlo simulation as an effective method to propagate the uncertainties in the finite element model of structure is applied to simulate the complicate situations that may occur. To improve efficiency of Monte Carlo simulation in sampling process, Latin Hypercube sampling is performed. However, the huge database of sampling is difficult to provide explicit evaluation of reliability. Polynomial chaos expansion is presented and discussed. Kriging model as a surrogate model play an important role in the reliability analysis.Traditional methods of optimization have disadvantages in unacceptable time-complexity or natural drawbacks of premature convergence because of finding the nearest local optima of low quality. Simulated Annealing is a local search-based heuristic, Genetic Algorithm draws inspiration from the principles and mechanisms of natural selection, that makes us capable of escaping from being trapped into a local optimum. In reliability based design optimization, these two methods were performed as the procedure of optimization. The loop of reliability analysis is running in surrogate model

L’objectif de la thèse est d’effectuer l’analyse de sensibilité paramétrique du logiciel Phast de modélisation de la dispersion atmosphérique de gaz toxiques et/ou inflammables. La technique a consisté à coupler Phast et l’outil d’analyse de sensibilité SimLab, ce qui permet d’exécuter automatiquement un grand nombre de simulations en faisant varier l’ensemble des paramètres du modèle de façon simultanée. La méthode d’analyse de sensibilité globale choisie, E-FAST, est basée sur l’analyse de la variance des sorties du modèle pour le calcul des indices de sensibilité. Nous avons étudié des scénarios de rejet continus pour six produits différents (monoxyde d’azote, ammoniac, chlore, azote, n-hexane et fluorure d’hydrogène), sélectionnés pour couvrir une large gamme de caractéristiques physiques et de conditions de stockage. L’analyse du modèle de dispersion de Phast, Unified Dispersion Model, a été séparée en deux étapes : étape de « screening » avec pour but de comparer l’influence de l’ensemble des paramètres puis étude de l’influence globale des paramètres de modélisation, autres que les paramètres météo et du terme source, sur une plage large de valeurs. Pour chaque produit, nous avons décomposé les scénarios de base en sous-scénarios correspondant à des conditions de rejet différentes. Ce travail a notamment permis de classifier les paramètres du modèle selon leur degré d’influence sur la variabilité de différentes sorties et d’effectuer une analyse comparative par produit indiquant, pour des conditions de rejet données, quels paramètres sont les plus influents sur les sorties. Une étude complémentaire a consisté à effectuer une analyse de sensibilité locale de ces paramètres autour de leur valeur par défaut
We have undertaken a parametric sensitivity analysis of the Phast software tool’s models for atmospheric dispersion of toxic and/or inflammable gases. We have coupled Phast with the sensitivity analysis tool SimLab, and have automated the execution of a large number of simulations while varying simultaneously selected model parameters. The global sensitivity analysis method used, E-FAST, is based on analysis of the variance of model outputs, and allows us to estimate sensitivity indices. We have studied continuous release scenarios for six different products (nitric oxide, ammonia, chlorine, nitrogen, n-hexane and hydrogen fluoride), which were chosen to cover a wide range of physical characteristics and storage conditions. Our analysis of Phast’s Unified Dispersion Model comprises two phases: a screening phase which allows the sensitivity of a wide range of parameters to be compared, followed by a phase focusing on the sensitivity of internal model parameters (excluding weather and source term variables), over a wide input range. For each product, we have broken down base-case scenarios into a number of sub-scenarios corresponding to different release conditions. This work has allowed us to rank model parameters according to their influence on the variability of a number of model outputs. It also includes a per-product comparative analysis indicating, for each release condition studied, which parameters have the most influence on the outputs. In the final part of the work, we have analyzed the local sensitivity of these parameters in a narrow range around their default values

Un système robotique est un système complexe, à la fois d’un point de vue matériel et logiciel. Afin de simplifier la conception de ces machines, le développement est découpé en modules qui sont ensuite assemblés pour constituer le système complet. Cependant, la facilité de conception de ces systèmes est bien souvent contrebalancée par la complexité de leur mise en sécurité, à la fois d’un point de vue fonctionnel et temporel. Il existe des ensembles d’outils et de méthodes permettant l’étude d’ordonnançabilité d’un système logiciel à base de tâches. Ces outils permettent de vérifier qu’un système de tâches respecte ses contraintes temporelles. Cependant ces méthodes d’analyse considèrent les tâches comme des entités monolithiques, sans prendre en compte la structure interne des tâches, ce qui peut les rendre trop pessimistes et non adaptées à des applications robotiques. Cette étude consiste à prendre en compte la structure interne des tâches dans des méthodes d’analyse d’ordonnançabilité. Cette thèse montre que le découpage de tâches monolithiques permet d’améliorer la précision des analyses d’ordonnancement. De plus, les outils issus de ces travaux ont été expérimentés sur un cas d’application de robotique mobile autonome
A robot is a complex system combining hardware and software parts. In order to simplify the robot design, the whole system is split in several separated modules. However, the complexity of the functional and temporal validation to improve the safety counterweights the robot design simplicity. We can find scheduling analysis tools for task-based software. These tools are used to check and validate the schedulability of the tasks involved in a software, run on a specific hardware. However, these methods considers the tasks as monolithic entities, without taking into account their internal structure. The resulting analyses may be too much pessimistic and therefore not applicable to robotic applications. In this work, we have modeled the internal structure of the tasks as state-machines and used these state-machines into the schedulability analysis in order to improve the analysis precision. Moreover, the tools developed during this work have been tested on real robotic use-cases

Deux solutions de protection utilisant la carte a microcalculateur ont ete etudiees. L'une est une protection d'acces a la machine. La deuxieme protege le logiciel en chiffrant une partie de ses instructions. Ces solutions ont ete validees par deux maquettes associant du materiel et du logiciel afin de proteger des attaques des utilitaires pour ibm pc

De nos jours, l'augmentation de la complexité des systèmes embarqués impose la prise en charge, dès les premiers prototypes et au niveau logiciel, d'exigences habituellement traitées plus tardivement voire même seulement lors du passage en série, comme notamment les contraintes de sûreté de fonctionnement. Nous proposons une méthodologie de développement de logiciels embarqués pouvant répondre aux besoins et contraintes de développement de ces logiciels dans la phase de prototypage. La flexibilité de la méthodologie garantit une meilleure gestion des évolutions récurrentes caractérisant les logiciels dans cette phase de prototypage. Aussi, grâce à sa structure bien adaptée, l'aspect automatisé de son intégration et de sa mise en place, notre méthodologie garantit une réduction significative des coûts du passage en série et de la mise en place de normes telles que l'ISO 26262 ou la DO-178. Pour illustrer les résultats que nous obtenons grâce à notre méthodologie et la chaîne d'outils associée, nous l'appliquons dans le cadre d'un projet industriel d'innovation qui consiste à la robotisation d'un véhicule prototype. Le cas d'étude se concentre sur la fonction "accélérateur" de ce prototype
Nowadays, the increasing complexity of embedded systems requires the management, from the first prototypes and software level, of requirements usually handled later even only when passing in production, such as including dependability constraints. We propose a development methodology for embedded software that can meet the needs and constraints of developing this software in the prototyping phase. The flexibility of the methodology ensures better management of recurring changes characterizing the software in the prototyping phase. Also, due to its well-adapted structure, and automated aspect of its integration and implementation, our methodology ensures a significant cost reduction of serialization and implementation of norms such as ISO 26262 or DO-178. To illustrate the results, we apply our methodology and the associated toolchain to an innovative industrial project which consists to robotize a prototype car. The case study focuses on the accelerator function of the prototype

Afin de dissuader les eventuels detournements de matieres nucleaires, un inspecteur est charge d'effectuer un certain nombre d'inspections dans une installation nucleaire. Deux inspections ont lieu a des dates fixes et connues de l'inspecteur et d'un eventuel detourneur. Entre les deux dates, un nombre limite d'inspections peuvent etre decidees par l'inspecteur. Nous supposons qu'un detournement est toujours detecte lors de l'inspection suivante. L'inspecteur cherche a minimiser le temps de detection et l'eventuel detourneur a le maximiser. Les jeux d'inspections sont etudies en deux temps. Nous considerons d'abord differentes familles de jeux d'inspection, et nous nous interessons tout particulierement aux jeux admettant une structure recursive. Ensuite, nous elaborons un jeu a information incomplete repondant aux donnees du probleme pose et realisons un logiciel, nomme jadis, permettant d'obtenir des strategies optimales d'inspection sur un grand nombre de periodes. Le jeu peut alors etre etudie sur un nombre de periodes suffisamment large pour confirmer le fait que l'information incomplete permet de reduire le temps de detection d'un detournement. Un second type de jeu est egalement etudie, le jeu d'infiltration, qui consiste en une poursuite-evasion sur un graphe de plusieurs arcs reliant deux noeuds. Un agent infiltrant doit se rendre de l'un de ces deux noeuds a l'autre sans etre intercepte par un gardien. Differents contextes de surveillance sont etudies.

Dans le contexte du développement de logiciels automobiles, le problème général qui a motivé ce travail était la complexité croissante des architectures logicielles et les limites des pratiques actuelles en termes d’analyses de sécurité. Malgré le développement du MBSE (Model Based Systems Engineering), ces pratiques sont toujours caractérisées par le recours à des techniques manuelles traditionnelles d’analyse de la sécurité telles que l’analyse par arbre de défaillance (FTA) ou l’analyse des modes de défaillance et de leurs effets (AMDE). Bien qu’elles soient toujours utiles, ces techniques sont insuffisantes face à la complexité avec la possibilité d’aboutir à des analyses subjectives, inefficaces, de mauvaise qualité et sujettes aux erreurs. Par conséquent, pour améliorer l’état de la pratique actuelle dans le contexte automobile, notre proposition est d’appliquer l’approche d’analyse de la sécurité basée sur un modèle (MBSA) qui est une approche d’ingénierie pilotée par modèle pertinente appliquée à la sécurité. Toutefois, l’examen de l’état actuel de la technique des approches actuelles des MBSA suggère que la plupart de ces approches sont axées sur les systèmes et manquent d’un soutien méthodologique clair. En outre, certaines des approches MBSA (en particulier celles qui reposent sur un modèle dédié) nécessitent une compréhension approfondie (en termes de paradigme de modélisation) et peuvent être difficiles à mettre en œuvre dans le cas de systèmes complexes (limites de la modélisation manuelle). De même, dans les pratiques actuelles, l’analyse de la sécurité au niveau logiciel souffre d’une mauvaise intégration avec le processus de développement logiciel, ce qui peut entraîner des analyses de sécurité incohérentes. Pour résoudre ces problèmes, l’essence de notre contribution est de fournir une méthodologie qui adapte les concepts, les principes et les méthodes de MBSA dans le but d’améliorer la pratique de l’analyse de la sécurité des logiciels, en tenant compte de l’état actuel des pratiques (dans le processus de développement de logiciels existant).Notre première contribution consiste en une méthodologie couvrant toutes les étapes nécessaires pour effectuer une analyse de la sécurité sur les architectures logicielles automobiles en utilisant l’approche basée sur des modèles tout en répondant aux défis présentés par le manque d’intrants inadéquats apportés par l’utilisation d’artefacts centrés sur les documents dans certaines parties du processus de génie logiciel. Grâce à cette contribution, nous proposons une méthodologie étape par étape pour définir le contexte d’analyse de la sûreté, construire l’architecture dysfonctionnelle et l’utiliser pour des analyses de sûreté s’appuyant sur une approche modèle dédiée.La deuxième proposition, également méthodologique, vise à relever certains défis liés à la complexité due aux limites d’une approche modèle dédiée. Elle consiste à utiliser des modèles de pannes logicielles basés sur des modèles de pannes logicielles ISO 26262 pour faciliter la construction du modèle dysfonctionnel. Grâce à cette proposition, des prototypes de modèles de défaillance logicielle courants sont développés et réutilisés pour construire le modèle dysfonctionnel.La troisième contribution, encore en cours de développement, est une proposition d’outillage visant à automatiser partiellement et à faciliter la construction du comportement et de la propagation des défauts des composants logiciels par traduction logique fonctionnelle à dysfonctionnelle. Il vise à assurer une meilleure cohérence des analyses de sécurité logicielle avec le processus de développement logiciel en permanence avec les recommandations ISO 26262
In the context of automotive software development, the general problem that motivated this work was the growing complexity of software architectures and the limitations of the current practices in terms of safety analyses. Despite the development of MBSE (Model Based Systems Engineering), these practices are still characterized by the reliance on manual traditional safety analysis techniques such as Fault Tree Analysis (FTA) or Failure Modes and Effect Analysis (FMEA). Although still useful, these techniques fall short when faced with complexity with the possibility of resulting in subjective, inefficient, poor quality and error-prone analyses. Hence, to improve the state of the current practice in the automotive context, our proposal is to apply the Model Based Safety Analysis (MBSA) approach that is a relevant Model Driven Engineering approach applied to safety. However, the review of the current state of the art of current MBSA approaches suggests that most of these approaches are systems oriented and lack clear methodological support. In addition, some of the MBSA approaches (especially those relying on a dedicated model) require deep understanding (in terms of modeling paradigm) and can be challenging to implement in the case of complex systems (limitations of manual modeling). Also in current practices, safety analysis at software level suffers of poor integration with the software development process, which can result in inconsistent safety analyses. To address these issues, the essence of our contribution is to provide a methodology that adapts the concepts, principles, and methods of MBSA for the purpose of improving the practice of software safety analysis, taking into consideration the current state of practices (in the existing software development process).Our first contribution consists of a methodology covering all the steps required to perform safety analysis on automotive software architectures using the model-based approach while addressing the challenges presented by the lack of inadequate inputs brought by the use of document-centric artifact in some parts of the software engineering process. Through this contribution, we propose a step-by-step methodology for defining the safety analysis context, constructing the dysfunctional architecture, and using it for safety analyses relying on a dedicated model approach.The second proposal, also methodological, aims to address some challenges related to complexity brought by the limitations of a dedicated model approach. It consists of using software fault patterns based on ISO 26262 software fault templates to ease the construction of the dysfunctional model. Through this proposal, prototypes of common software fault patterns are developed and reused to build the dysfunctional model.The third contribution, still undergoing development, is a tooling proposal to partially automated and ease the construction of software component’s fault behavior and propagation through functional to dysfunctional logic translation. It aims to ensure a better consistency of software safety analyses with the software development process constantly with ISO 26262 recommendations

Cette thèse propose des solutions automatiques et modulaires aux trois problèmes principaux à résoudre pour appliquer les techniques de preuve déductive aux programmes C, dans le but de prouver l'absence de faille de sécurité exploitant une corruption mémoire. Ces problèmes sont la génération d'annotations logiques, la séparation mémoire et la prise en compte des unions et des casts. La preuve déductive repose sur la présence d'annotations logiques dans les programmes, qu'il n'est pas possible en pratique d'ajouter à la main en totalité. Nous proposons une méthode de génération d'annotations logiques basée sur les techniques d'interprétation abstraite, de calcul de plus faibles préconditions et d'élimination de quantificateurs. En présence de pointeurs, la preuve déductive n'est suffisamment précise que si les régions mémoires pointées sont disjointes. Nous proposons une méthode de séparation des régions mémoires basée sur une version contextuelle de l'analyse de Steensgaard, dont la correction est assurée par la génération de préconditions supplémentaires. En présence d'unions et de casts, les hypothèses habituelles de séparation entre champs de structures faites en preuve déductive ne sont plus valables. Nous proposons une classification des unions et des casts en C, ainsi qu'une articulation entre modèle mémoire typé et modèle mémoire bas-niveau qui permettent de retrouver les hypothèses habituelles de séparation. L'implantation de ces techniques dans les plate-formes Frama-C et Why a permis entre autre de trouver des bugs de sûreté mémoire et de vérifier les versions corrigées de bibliothèques existantes de chaînes de caractères
In this PhD thesis, we present automatic and modular solutions to the three main problems that come up when applying deductive verification techniques to C programs, in order to prove the absence of security flaws that exploit memory corruption. These problems are the generation of logical annotations, memory separation and the treatment of unions and casts. Deductive verification relies on the presence of logical annotations in programs. In practice, it is not possible to add all annotations manually. We propose a technique to generate such annotations based on abstract interpretation, weakest precondition calculus and quantifier elimination. When programs contain pointers, deductive verification is precise enough only if memory regions pointed-to are disjoint. We propose a technique to separate memory regions based on a contextual version of Steensgaard's alias analysis, whose correction is guaranteed by generating additional preconditions. When programs contain unions and casts, the usual hypothesis made in deductive verification that fields of structures are separated is not valid anymore. We propose a classification of unions and casts, as well as a combination of typed memory model and byte-level memory model, that validates the usual hypothesis of field separation. We have implemented these techniques in Frama-C and Why platforms. By applying them to the verification of existing libraries for strings, we both managed to find memory safety bugs in the original versions and to check the safety of corrected versions of the same libraries

Ces dernières années, le monde des systèmes critiques a connu un véritable essor en matière de demande de logiciels. Dans une optique majeure de réduction des coûts de développement, les grands acteurs du monde critique comme ceux de l’avionique et de l’automobile s’orientent de plus en plus vers l’ingénierie dirigée par les modèles. Par contre les acteurs du domaine ferroviaire, pour des raisons stratégiques et organisationnelles restent encore fidèles à des méthodes conventionnelles qui leur permettent de tirer au maximum profit de leurs compétences. Cependant, ces approches conventionnelles souffrent d’un manque d’abstraction pour la traçabilité des préoccupations et la vérification formelle, qui sont fortement recommandées dans le développement des logiciels critiques dans le domaine ferroviaire. Pour faire face à ces limitations, nous présentons dans cette thèse une approche systématique basée sur l’ingénierie dirigée par les modèles à base de composants, de façon à maîtriser au mieux la complexité des logiciels et la traçabilité des préoccupations. Nous proposons notamment trois contributions essentielles. En premier lieu, nous fournissons un ensemble uniformisé de méta-modèles permettant de décrire les préoccupations des exigences logicielles, les composants logiciels, et la traçabilité entre les préoccupations et ces composants logiciels. Avec la deuxième contribution, nous proposons un support formel de notre modèle pour en permettre la vérification formelle. Finalement, la dernière contribution propose une approche de développement et de vérification à base de composants logiciels, nommée SARA pour "SAfety-critical RAilway control applications". Nous avons validé notre approche avec quelques cas d’études du nouveau système européen de contrôle de train, ERTMS/ETCS
In recent years, the development of critical systems demands more and more software. In order to reduce their costs of development and verification, actors in critical domains, such as avionics and automotive domains, are moving more and more towards model-driven engineering. In contrast, in the railway domain, for strategic and organizational reasons, actors remain faithful to traditional methods that allow them to take advantage of their knowledge. However, these conventional approaches suffer from a lack of abstraction and do not provide supports for traceability of concerns and formal verification, which are highly recommended for the development of railway safety-critical software. To address these shortcomings, we present in this thesis a systematic approach based on model driven engineering and component-based model, in order to better manage software complexity and traceability of concerns. In this dissertation, we provide in particular three major contributions. First, we provide an integrated set of meta-models for describing the concerns of software requirements, software components, and traceability between the concerns and software components. With the second contribution, we propose a formal support of our model to allow formal verification of temporal properties. Finally, with the last contribution, we propose a software component-based development and verification approach, called SARA, and included in V-lifecycle widely used in the railway domain. Experiments we conducted to validate our approach through a few case studies of the new European train control system ERTMS/ETCS, show that by using component model that explicitly include requirement traceability, we are able to provide a practical, scalable and reliable approach

Objective: In order to introduce automated vehicles on public roads, it is necessary to ensure that these vehicles are safe to operate in traffic. One challenge is to prove that all physically possible variations of situations can be handled safely within the operational design domain of the vehicle. A promising approach to handling the set of possible situations is to identify a manageable number of logical scenarios, which provide an abstraction for object properties and behavior within the situations. These can then be transferred into concrete scenarios defining all parameters necessary to reproduce the situation in different test environments. Methods: This article proposes a framework for defining safety-relevant scenarios based on the potential collision between the subject vehicle and a challenging object, which forces the subject vehicle to depart from its planned course of action to avoid a collision. This allows defining only safety-relevant scenarios, which can directly be related to accident classification. The first criterion for defining a scenario is the area of the subject vehicle with which the object would collide. As a second criterion, 8 different positions around the subject vehicle are considered. To account for other relevant objects in the scenario, factors that influence the challenge for the subject vehicle can be added to the scenario. These are grouped as action constraints, dynamic occlusions, and causal chains. Results: By applying the proposed systematics, a catalog of base scenarios for a vehicle traveling on controlled-access highways has been generated, which can directly be linked to parameters in accident classification. The catalog serves as a basis for scenario classification within the PEGASUS project. Conclusions: Defining a limited number of safety-relevant scenarios helps to realize a systematic safety assurance process for automated vehicles. Scenarios are defined based on the point of the potential collision of a challenging object with the subject vehicle and its initial position. This approach allows defining scenarios for different environments and different driving states of the subject vehicle using the same mechanisms. A next step is the generation of logical scenarios for other driving states of the subject vehicle and for other traffic environments.

Ce travail a porté sur l'élaboration d'un modèle et d'un logiciel de simulation du mouvement de personnes évacuant un bâtiment, lors d'un incendie ou bien à l'occurrence d'une autre situation dégradée justifiant l'évacuation ou la provoquant spontanément. Un algorithme original a été développé, applicable à de fortes densités de personnes dans un environnement complexe comprenant des obstacles au mouvement. Un maillage sert de trame pour représenter, outre les aires offertes au déplacement, les murs et autres obstacles, qu'ils soient matériels ou qu'ils représentent des régions dangereuses. Le logiciel développé simule le déplacement des occupants évoluant en coordonnées continues dans un environnement complexe et interagissant au niveau de la vitesse de leur déplacement ainsi que de la densité maximale d'occupation qu'il est possible d'atteindre. Ce modèle a pu être réalisé au moyen d'une application locale, au niveau du micro-environnement de chaque occupant, des lois de corrélation macroscopiques vitesse-densité identifiées par plusieurs auteurs. L'utilisation d'un post-processeur graphique mis au point lors de ce travail, a rendu possible la mise en évidence des phénomènes inhérents au mouvement de foule (accumulation, blocage, détente,)

Les travaux présentés dans cette thèse constituent une contribution aux méthodes de génération automatique de sous-approximations en vue de la génération de tests a` partir de modèles. Le test à partir de modèle a pour objectif de garantir la conformité d’une implémentation vis-à-vis d’un modèle, tous les deux conçus à partir des spécifications par deux équipes différentes.Dans cette thèse, nous proposons l’utilisation des techniques connues d’abstraction à partir de prédicats de modèles comportementaux qui permettent de réduire à un ensemble fini et restreint l’espace d’états manipulé. Nous proposons d’extraire les prédicats d’abstraction à partir de l’objectif de test afin que les tests générés couvrent les comportements ciblés par ce dernier. Cependant, le calcul d’une abstraction entraîne une perte d’information de l’atteignabilité par rapport au modèle initial. Nos objectifs sont donc dans un premier temps de calculer efficacement une abstraction de modèle aussi représentative que possible d’un objectif de test. Dans un second temps, nous cherchons a` extraire a` partir de cette abstraction des exécutions instanciables sur le modèle avant abstraction, ciblant les comportements a` tester, et visant la couverture des états et des transitions du modèle abstrait.Nos contributions sont les suivantes. Nous définissons une méthode de génération de tests combinant plusieurs algorithmes qui permettent d’obtenir une bonne couverture structurelle d’une abstraction de modèle comportemental non déterministe. Nous proposons dans un premier temps un algorithme calculant une abstraction de modèle par prédicats issus d’un objectif de test exprime´ sous la forme d’une propriétée temporelle. Cet algorithme calcule une sous-approximation du modèle en couvrant les états et les transitions abstraits du modèle. Il applique plusieurs heuristiques et diverses techniques d’exploration ayant pour but d’augmenter le nombre d’instances effectivement atteintes. Dans un second temps, nous proposons d’améliorer par le biais de deux autres algorithmes la couverture structurelle obtenue par cette première sous-approximation. Le premier, entièrement automatisé, tire parti des modalités des transitions abstraites qui fournissent des propriétés d’atteignabilité. Le second algorithme d’extension de la sous-approximation fait appel à l’expertise du testeur qui doit, a` partir des transitions non couvertes, énoncer un prédicat de pertinence qui guide et limite l’exploration et l’instanciation réalisées. Nous définissons un ensemble de règles permettant d’énoncer ce prédicat de pertinence et de calculer un variant garantissant la terminaison de l’algorithme d’exploration. Ces deux algorithmes complètent la sous-approximation obtenue auparavant par des exécutions instanciables. Enfin, nous mettons en œuvre une démarche expérimentale pour l’évaluation de la qualité de la méthode, portant sur cinq études de cas
The work presented in this thesis contributes to the automated under-approximation generation techniques in order to generate tests from models.Model based testing aims at guaranteeing the conformity of an implementation with regards to a model, both designed from specifications by two distinct teams.In this thesis, we propose to use well known abstraction techniques by using predicates extracted from behavioural models allowing to reduce the manipulated state space to a finite and narrow set. We propose to extract the abstraction predicates from the test purpose so that the generated tests cover the behaviours it targets. However, the computation of an abstraction causes a loss of information of the reachability with regards to the initial model. Our goals are, on the one hand, to efficiently compute an abstraction of the model as representative as possible of a test purpose. On the other hand, we strive to extract executions from this abstraction which can be instanciated on the model before its abstraction, targeting the behaviours to test, and aiming at covering the states and the transitions of the abstracted model.Our contributions are the following. We define a test generation method combining various algorithms allowing to obtain a good structural coverage of the abstraction of a non deterministic behavioural model. We first propose an algorithm computing the abstraction of a model using predicates extracted from a test purpose expressed as a temporal property. This algorithm computes an under-approximation of the model by covering the abstract states and transitions of the model. It applies various exploration heuristics and techniques with the aim of increasing the amount of reached instances. Then, we propose to improve by the means of two other algorithms the structural coverage obtained by this first under-approximation. The first of these algorithms, fully automated, takes advantage of the known modalities of the abstract transitions which provide us with reachability properties. The second under-approximation extension algorithm uses the expertise of the tester who must, from non covered transitions, design a relevance predicate which will guide and limit the exploration and the instanciations. We define a set of rules allowing to express this relevance predicate and compute a variant guaranteeing the termination of the exploration algorithm. These two algorithms complete the under-approximation by necessarily instanciable executions. Finally, we experimentally assess the quality of the method on five case studies

Dans cette thèse, nous analysons les problèmes liés à la représentation finie des nombres réels et nous contrôlons la déviation induite par cette approximation. Nous nous intéressons particulièrement à deux problèmes. Le premier est l'étude de l'influence de la représentation finie sur les protocoles de confidentialité différentielle. Nous présentons une méthode pour étudier les perturbations d'une distribution de probabilité causées par la représentation finie des nombres. Nous montrons qu'une implémentation directe des protocoles théoriques pour garantir la confidentialité différentielle n'est pas fiable, tandis qu'après l'ajout de correctifs, la propriété est conservée en précision finie avec une faible perte de confidentialité. Notre deuxième contribution est une méthode pour étudier les programmes qui ne peuvent pas être analysés par composition à cause de branchements conditionnels au comportement trop erratique. Cette méthode, basée sur la théorie des systèmes de réécriture, permet de partir de la preuve de l'algorithme en précision exacte pour fournir la preuve que le programme en précision finie ne déviera pas trop
In this thesis, we analyze the problem of the finite representation of real numbers and we control the deviation due to this approximation. We particularly focus on two complex problems. First, we study how finite precision interacts with differentially private protocols. We present a methodology to study the perturbations on the probabilistic distribution induced by finite representation. Then we show that a direct implementation of differential privacy protocols is not safe while, with addition of some safeguards, differential privacy is preserved under finite precision up to some quantified inherent leakage. Next, we propose a method to analyze programs that cannot be analyzed by a compositional analysis due to ''erratic'' control flow. This method based on rewrite system techniques allows us to use the proof of correction of the program in the exact semantics to prove the program is still safe in the finite representation

Ce travail porte sur une approche multi perspectives pour la conception des systèmes interactifs critiques appelée « Generic Integrated Modelling Framework ». Le but est de proposer des techniques, méthode et outils pour une conception basée sur des modèles prenant en compte les comportements erronés du système et des utilisateurs. Notre recherche se concentre sur la modélisation des tâches et du système qui, comme d'autres modèles, sont souvent développés pour des cas d'utilisation normale, sans prendre en compte ni les erreurs humaines ni les comportements erronés du système. Ces modèles sont souvent réalisés par des experts de compétences et de cultures différentes, et il est peu probable qu’ils soient substituables. Nous avons conçu une approche permettant d'intégrer au moyen de modèles (principalement tâches et système) des informations sur les comportements incorrects des utilisateurs et du système. Cette perspective repousse les frontières du développement basé sur des modèles, du fait que ces informations additionnelles permettent de prendre en compte des expériences d'échec. Le but final est l'amélioration du processus de conception dans le but de produire des systèmes interactifs plus fiables. Cette approche est appliquée à deux études de cas : Etude d’un accident mortel impliquant un système de gestion de carburant dans une usine de ciment. Etude d’une application interactive issue d’un cockpit interactif répondant à la norme ARINC 661. L’idée fondamentale est de rassembler dans un cadre unique des principes issus de la conception centrée utilisateur et du domaine des systèmes critiques
This thesis presents a multi-perspective approach for the design of interactive safety-critical systems called the « Generic Integrated Modelling Framework ». The goal is to propose techniques, methods and tools for the model-based design while taking into account human and system-related erroneous behaviour. Our research focuses on task and system modeling, which like other models, are often developed from an error-free perspective, without taking into account human or system errors. These models are often developed by experts with different backgrounds and cultures. It is thus unlikely that the data gathered, analysed and documented will be represented in the same way. We have developed an approach which allows the integration of erroneous behaviour of both the users and the system via models (notably the task and system model). This perspective extends the boundaries of model based design since this additional information allows us to take into account previous failures. The main aim is to improve the design process in order to produce safer safety-critical interactive systems. This approach has been applied to two case studies : A fatal mining accident involving a gas management system within a cement plant An interactive cockpit application meeting the requirements of the ARINC 661 specification. The fundamental idée is to bring together within a single framework principle issues of user centred design within the safety-critical domain

Synchronous languages such as Signal, Lustre and Esterel are dedicated to designing safety-critical systems. Their compilers are large and complicated programs that may be incorrect in some contexts, which might produce silently bad compiled code when compiling source programs. The bad compiled code can invalidate the safety properties that are guaranteed on the source programs by applying formal methods. Adopting the translation validation approach, this thesis aims at formally proving the correctness of the highly optimizing and industrial Signal compiler. The correctness proof represents both source program and compiled code in a common semantic framework, then formalizes a relation between the source program and its compiled code to express that the semantics of the source program are preserved in the compiled code.

Cette thèse a pour objectif de proposer une approche formelle basée sur les automates d'interface pour spécifier les contrats des composants réutilisables et vérifier leur interopérabilité fonctionnelle. Cette interopérabilité se traduit par la vérification des trois niveaux : signature, sémantique, et protocole. Le formalisme des automates d'interface est basé sur une approche " optimiste" qui prend en compte les contraintes de l'environnement. Cette approche considère que deux composants sont compatibles s'il existe un environnement convenable avec lequel ils peuvent interagir correctement. Dans un premier temps, nous proposons une approche préliminaire qui intègre la sémantique des paramètres des actions dans la vérification de la compatibilité et de la substitution des composants spécifiés par des automates d'interface. Dans un second temps, nous nous somme intéressés à adapter les composants réutilisables dont les contrats sont décrits par des automates d'interface enrichis par la sémantique des actions. En ce sens, nous avons proposé un algorithme qui permet de générer automatiquement la spécification d'un adaptateur de deux composants lorsque celui-ci existe. Dans un troisième temps, nous avons augmenté le pouvoir d'expression de notre approche proposée pour vérifier l'interopérabilité et les propriétés de sûreté des composants qui communiquent par des variables définies au niveau de leurs contrats d'interface. En particulier, nous étudions la préservation des invariants par composition et par raffinement.

Nous proposons dans cette thèse une nouvelle approche pour l'exploration d’espaces de conception. Plus précisément, nous utilisons la composition de transformations de modèles pour automatiser la production d'alternatives architecturales, et les algorithmes génétiques pour explorer et identifier des alternatives architecturales quasi-optimales. Les transformations de modèles sont des solutions réutilisables et peuvent être intégrées dans des algorithmes génétiques et ainsi être combinées avec des opérateurs génétiques tels que la mutation et le croisement. Grâce à cela, nous pouvons utiliser (ou réutiliser) différentes transformations de modèles implémentant différents patrons de conception sans pour autant modifier l’environnement d’optimisation. En plus de cela, les transformations de modèles peuvent être validées (par rapport aux contraintes structurelles) en amont et ainsi rejeter avant l’exploration les transformations générant des alternatives architecturales incorrectes. Enfin, les transformations de modèles peuvent être chainées entre elles afin de faciliter leur maintenance, leur réutilisabilité et ainsi concevoir des modèles plus détaillés et plus complexes se rapprochant des systèmes industrielles. A noter que l’exploration de chaines de transformations de modèles a été intégrée dans l’environnement d’optimisation
In this thesis, we propose a new exploration approach to tackle design space exploration problems involving multiple conflicting non functional properties. More precisely, we propose the use of model transformation compositions to automate the production of architectural alternatives, and multiple-objective evolutionary algorithms to identify near-optimal architectural alternatives. Model transformations alternatives are mapped into evolutionary algorithms and combined with genetic operators such as mutation and crossover. Taking advantage of this contribution, we can (re)-use different model transformations, and thus solve different multiple-objective optimization problems. In addition to that, model transformations can be chained together in order to ease their maintainability and re-usability, and thus conceive more detailed and complex systems

Nous proposons dans cette thèse une nouvelle approche pour l'exploration d’espaces de conception. Plus précisément, nous utilisons la composition de transformations de modèles pour automatiser la production d'alternatives architecturales, et les algorithmes génétiques pour explorer et identifier des alternatives architecturales quasi-optimales. Les transformations de modèles sont des solutions réutilisables et peuvent être intégrées dans des algorithmes génétiques et ainsi être combinées avec des opérateurs génétiques tels que la mutation et le croisement. Grâce à cela, nous pouvons utiliser (ou réutiliser) différentes transformations de modèles implémentant différents patrons de conception sans pour autant modifier l’environnement d’optimisation. En plus de cela, les transformations de modèles peuvent être validées (par rapport aux contraintes structurelles) en amont et ainsi rejeter avant l’exploration les transformations générant des alternatives architecturales incorrectes. Enfin, les transformations de modèles peuvent être chainées entre elles afin de faciliter leur maintenance, leur réutilisabilité et ainsi concevoir des modèles plus détaillés et plus complexes se rapprochant des systèmes industrielles. A noter que l’exploration de chaines de transformations de modèles a été intégrée dans l’environnement d’optimisation
In this thesis, we propose a new exploration approach to tackle design space exploration problems involving multiple conflicting non functional properties. More precisely, we propose the use of model transformation compositions to automate the production of architectural alternatives, and multiple-objective evolutionary algorithms to identify near-optimal architectural alternatives. Model transformations alternatives are mapped into evolutionary algorithms and combined with genetic operators such as mutation and crossover. Taking advantage of this contribution, we can (re)-use different model transformations, and thus solve different multiple-objective optimization problems. In addition to that, model transformations can be chained together in order to ease their maintainability and re-usability, and thus conceive more detailed and complex systems

L'objectif de ce travail est de proposer à des constructeurs des commances de machines à logique programmée une architecture redondante ayant un bon niveau de sécurité et présentant un coût de développement et de réalisation du même ordre de grandeur que ceux réalisés actuellement en logique électromécanique

Un logiciel critique est un logiciel dont le mauvais fonctionnement peut avoir un impact important sur la sécurité ou la vie des personnes, des entreprises ou des biens.L'ingénierie logicielle pour les systèmes critiques est particulièrement difficile et combine différentes méthodes pour garantir la qualité des logiciels produits.Parmi celles-ci, les méthodes formelles peuvent être utilisées pour prouver qu'un logiciel respecte ses spécifications.Le travail décrit dans cette thèse s'inscrit dans le contexte de la validation de propriétés de sûreté de programmes critiques, et plus particulièrement des propriétés numériques de logiciels embarqués dans des systèmes de contrôle-commande.La première partie de cette thèse est consacrée aux preuves de stabilité au sens de Lyapunov.Ces preuves s'appuient sur des calculs en nombres réels, et ne sont pas valables pour décrire le comportement d'un programme exécuté sur une plateforme à arithmétique machine.Nous présentons un cadre théorique générique pour adapter les arguments des preuves de stabilité de Lyapunov aux arithmétiques machine.Un outil effectue automatiquement la traduction de la preuve en nombres réels vers une preuve en nombres a virgule flottante.La seconde partie de la thèse porte sur l'analyse des relations affines, en utilisant une interprétation abstraite basée sur l'approximation des valuations associées aux points de contrôle d'un programme par des polyèdres convexes.Nous présentons ALICe, un framework permettant de comparer différentes techniques de génération d'invariants.Il s'accompagne d'une collection de cas de tests tirés de publications sur l'analyse de programmes, et s'interface avec trois outils utilisant différents algorithmes de calcul d'invariants: Aspic, iscc et PIPS.Afin d'affiner les résultats de PIPS, deux techniques de restructuration de code sont introduites, et plusieurs améliorations sont apportées aux algorithmes de génération d'invariants et évaluées à l'aide d'ALICe
A critical software is a software whose malfunction may result in death or serious injury to people, loss or severe damage to equipment or environmental harm.Software engineering for critical systems is particularly difficult, and combines different methods to ensure the quality of produced software.Among them, formal methods can be used to prove that a software obeys its specifications.This thesis falls within the context of the validation of safety properties for critical software, and more specifically, of numerical properties for embedded software in control-command systems.The first part of this thesis deals with Lyapunov stability proofs.These proofs rely on computations with real numbers, and do not accurately describe the behavior of a program run on a platform with machine arithmetic.We introduce a generic, theoretical framework to adapt the arguments of Lyapunov stability proofs to machine arithmetic.A tool automatically translates the proof on real numbers to a proof with floating-point numbers.The second part of the thesis focuses on linear relation analysis, using an abstract interpretation based on the approximation by convex polyhedrons of valuations associated with each control point in a program.We present ALICe, a framework to compare different invariant generation techniques.It comes with a collection of test cases taken from the program analysis literature, and interfaces with three tools, that rely on different algorithms to compute invariants: Aspic, iscc and PIPS.To refine PIPS results, two code restructuring techniques are introduced, and several improvements are made to the invariant generation algorithms and evaluated using ALICe

With the advent of cloud computing and Software-as-a-Service, Service-Based Application (SBA) represents a new paradigm to build rapid, low-cost, interoperable and evolvable distributed applications. A new application is created by defining a workflow that coordinates a set of third-party Web services accessible over the Internet. In such distributed and loose coupling environment, the execution of SBA requires a high degree of flexibility. For example, suitable constituent services can be selected and integrated at runtime based on their Quality of Service (QoS); furthermore, the composition of service is required to be dynamically modified in response to unexpected runtime failures. In this context, the main objective of this dissertation is to design, to develop and to evaluate a service middleware for flexible execution of SBA by using chemical programming model. Using chemical metaphor, the service-based systems are modeled as distributed, selforganized and self-adaptive biochemical systems. Service discovery, selection, coordination and adaptation are expressed as a series of pervasive chemical reactions in the middleware, which are performed in a distributed, concurrent and autonomous way. Additionally, on the way to build flexible service based systems, we do not restrict our research only in investigating chemical-based solutions. In this context, the second objective of this thesis is to find out generic solutions, such as models and algorithms, to respond to some of the most challenging problems in flexible execution of SBAs. I have proposed a two-phase online prediction approach that is able to accurately make decisions to proactively execute adaptation plan before the failures actually occur.

En France, les chutes constituent la première cause de mortalité chez les plus de 75 ans, et la seconde chez les plus de 65 ans. On estime qu'elle engendre un coût de 1 à 2 milliards d'euros par an pour la société. L'enjeu humain et socio-économique est colossal, sachant que le risque de chute est multiplié par 20 après une première chute, que le risque de décès est multiplié par 4 dans l'année qui suit une chute, que les chutes concernent 30% des personnes de plus de 65 ans et 50% des personnes de plus de 85 ans, et que l'on estime que d'ici 2050, plus de 30% de la population sera âgée de plus de 65 ans. Cette thèse propose un dispositif de détection de présence au sol se basant sur l'analyse de cartes de profondeurs acquises en temps réel, ainsi qu'une amélioration du dispositif proposé utilisant également un capteur thermique. Les cartes de profondeurs et les images thermiques nous permettent de nous affranchir des conditions d'illumination de la scène observée, et garantissent l'anonymat des personnes qui évoluent dans le champ de vision du dispositif. Cette thèse propose également différentes méthodes de détection du plan du sol dans une carte de profondeurs, le plan du sol constituant une référence géométrique nécessaire au dispositif proposé. Une enquête psychosociale a été réalisée, qui nous a permis d'évaluer l'acceptabilité a priori dudit dispositif. Cette enquête a démontré sa bonne acceptabilité, et a fourni des préconisations quant aux points d'amélioration et aux écueils à éviter. Enfin, une méthode de suivi d'objets dans une carte de profondeurs est proposée, un objectif à plus long terme consistant à mesurer l'activité des individus observés
In France, fall is the first death cause for people aged 75 and more, and the second death cause for people aged 65 and more. It is considered that falls generate about 1 to 2 billion euros health costs per year. The human and social-economical issue is crucial, knowing that for the mentioned populations, fall risk is multiplied by 20 after a first fall; that the death risk is multiplied by 4 in the year following a fall; that per year, 30% of the people aged 65 and more and 50% of the people aged 85 and more are subject to falls; and that it is estimated that more than 30% of the French population whill be older than 65 years old by 2050. This thesis proposes a ground lying event detection device which bases on the real time analysis of depth maps, and also proposes an improvement of the device, which uses an additional thermal sensor. Depth maps and thermal images ensure the device is independent from textures and lighting conditions of the observed scenes, and guarantee that the device respects the privacy of those who pass into its field of view, since nobody can be recognized in such images. This thesis also proposes several methods to detect the ground plane in a depth map, the ground plane being a geometrical reference for the device. A psycho-social inquiry was conducted, and enabled the evaluation of the a priori acceptability of the proposed device. This inquiry demonstrated the good acceptability of the proposed device, and resulted in recommendations on points to be improved and on pitfalls to avoid. Last, a method to separate and track objects detected in a depth map is proposed, the measurement of the activity of observed individuals being a long term objective for the device

The diploma thesis deals with realization of an Ayurvedic pavilion in the premises of Saint Katerina Resort. The proposed new compound is designed to extend the leisure services of the Saint Katerina Resort in Počátky. The feasibility study of the main technological stages of the project is solved in this diploma thesis. The construction of the object is described in the technical report. Both a detailed itemized budget of the construction and a detailed timetable to show the duration of each process is elaborated for the construction technology project. Futhermore, the design of site construction equipment, design of machine assembly, time deployment of machines and staff balance is elaborated. The project includes a technological regulation of the realization of the skeleton supporting frame structure and both control and test schedule. The work safety for the assembly of the wooden building supporting frame is composed.

Cette thèse s'inscrit dans la démarche de preuve de programmes à l'aide de vérification déductive. La vérification déductive consiste à produire, à partir des sources d'un programme, c'est-à-dire ce qu'il fait, et de sa spécification, c'est-à-dire ce qu'il est sensé faire, une conjecture qui si elle est vraie alors le programme et sa spécification concordent. On utilise principalement des démonstrateurs automatiques pour montrer la validité de ces formules. Quand ons'intéresse à la preuve de programmes qui utilisent des structures de données allouées en mémoire, il est élégant et efficace de spécifier son programme en utilisant la logique de séparation qui est apparu il y a une dizaine d'année. Cela implique de prouver des conjectures comportant les connectives de la logique de séparation, or les démonstrateurs automatiques ont surtout fait des progrès dans la logique du premier ordre qui ne les contient pas.Ce travail de thèse propose des techniques pour que les idées de la logique de séparation puissent apparaître dans les spécifications tout en conservant la possibilité d'utiliser des démonstrateurs pour la logique du premier ordre. Cependant les conjectures que l'ont produit ne sont pas dans la même logique du premier ordre que celles des démonstrateurs. Pour permettre une plus grande automatisation, ce travail de thèse a également défini de nouvelles conversions entre la logique polymorphe du premier ordre et la logique multi-sortée dupremier ordre utilisé par la plupart des démonstrateurs.La première partie a donné lieu à une implémentation dans l'outil Jessie, la seconde a donné lieu à une participation conséquente à l'écriture de l'outil Why3 et particulièrement dans l'architecture et écriture des transformations qui implémentent ces simplifications et conversions.

Some mental states, such as fatigue, or sleepiness, are known to increase the potential of accidents in industry, and thus could decrease productivity, even increase cost for healthcare. The highest rate of industrial accidents is usually found among shift workers due to fatigue or extended work hours. When using machine tool or interacting with robotic system, the risk of injury increases due to disturbance, lapse in concentration, vigilance decline, and neglect of the risk during prolonged use. Usually, to guarantee safety of worker, the conventional means is to stop the machine when human presence is detected in the safeguarding area of machine tool or robot workspace. The popular human detection technologies exploit laser scanner, camera (or motion tracker), infrared sensor, open-door sensor, static pressure sensitive floor as described in CSA Z434 standard. Of course, in the field of robotic, human and robot are not allowed to work together in the same workspace. However, new industrial needs lead research to develop flexible and reactive chain production for enabling small quantity production or fast modification in product characteristics. Consequently, more efficient human-machine or human-robot collaboration under a safety condition could improve this flexibility. Our research project aims at detecting and analyzing human safety in industry in order to protect workers. Comparing to the conventional human protection methods, our research exploits Artificial Intelligence approach to track and monitor human head motion and mental state using an instrumented safety helmet, labelled as Smart Safety Helmet (SSH) in the following. The contribution of this thesis consists in the design of data fusion algorithm for the recognition of head motion and mental state, which can be used to analyze the potential risky states of workers. A Smart Safety Helmet embedded with Inertial Measurement Unit (IMU) and EEG sensors will be used to detect and decode the human’s mental state and intention. The acquired information will be used to estimate the accident risk level in order to stop machine and then prevent accident or injury. In human-robot interaction (HRI) paradigm, the human’s intention could be used to predict the worker trajectory in order to control the robot moving trajectory and then to avoid fatal collision. Certains états mentaux, comme la fatigue ou la somnolence, sont connus pour augmenter le potentiel d'accidents dans l'industrie, et pourrait donc réduire la productivité, même augmenter les coûts des soins de santé. Le taux le plus élevé d'accidents au travail est habituellement trouvé parmi les travailleurs en rotation (travail posté) dues à la fatigue ou les heures de travail prolongées. Lors de l'utilisation d’une machine-outil ou lors d’une interaction avec un système robotique, le risque de lésion peut augmenter dû à une perturbation, un manque de concentration, une baisse de vigilance et la négligence du travailleur face au risque présent lors d'une utilisation prolongée (accoutumance au risque). Habituellement, pour garantir la sécurité des travailleurs, des moyens classiques sont l'arrêt complet de la machine lorsque la présence humaine est détectée dans une zone non sécuritaire, par exemple dans l’espace de travail d’un robot. Les technologies industrielles communes de détection humaine exploitent le scanner au laser, la caméra (par la capture de mouvement), le capteur infrarouge, l’interrupteur de porte ouverte, le tapis de capture de la pression statique ; tous ces capteurs sont décrits dans la norme CSA Z434. Jusqu’à tout récemment, dans le domaine de la robotique industrielle, les humains et les robots n’étaient pas autorisés à travailler ensemble dans le même espace. Toutefois, des besoins industriels émergents ont dirigé les recherches pour développer une production flexible et réactive pour favoriser la production de petites quantités ou modifier rapidement des caractéristiques du produit. Par conséquent, une collaboration plus efficace entre l'humain et le robot ou, de manière plus générale entre l'humain et la machine, sous des contraintes de sécurité, pourrait améliorer cette flexibilité et cette réactivité. Notre projet de recherche vise à détecter et à analyser la sécurité humaine dans l'industrie afin de protéger les travailleurs. En comparant les méthodes classiques de protection humaine, notre approche exploite l'intelligence artificielle pour identifier les mouvements de la tête et identifier l'état mental en utilisant un casque de sécurité instrumenté, nommé le Smart Safety Helmet (SSH) dans ce qui suit. La contribution de ce mémoire réside dans la conception de la fusion des données provenant de la reconnaissance de mouvement de la tête et de l'état mental, qui peut être utilisée pour analyser le potentiel de risque encouru par un travailleur. Dans le SSH, une unité de mesure inertielle (IMU) et capteurs EEG ont été intégrés. Ces deux capteurs seront utilisés pour détecter l'état mental de l’humain et décoder son intention. Les informations recueillies seront utilisées pour estimer le risque d'accidents afin d'arrêter la machine et d'empêcher un accident. Dans le paradigme de l’interaction humain-robot, l'intention de l'humain pourrait être utilisée modifier le comportement du robot (réduire sa rigidité ou modifier sa trajectoire).

碩士
元智大學
資訊工程學系
96
Safety and Security are the characteristics of software systems. For Safety systems, there is already a standard, namely, “Common Criteria, CC” for creating, inspecting or evaluating security requirement documents. For Security systems, however, there are no such standards so far. In this paper, we proposed to a common- standard-like approach to safety systems. We developed the logical structures for IEEE 603, a safety standard for nuclear power station. The logical structures include threats, critical asset constraints, defensive measures, and assurance as the top level components. The common-criteria-like classes, families, and components are then designed. Case studies using this approach have been conducted. Our approach improved the efficiency of the review process for the conformance of IEEE safety standard. Therefore, the safety of the reviewed system can then be enhanced.