Search

National audience; Un système autonome doit accomplir des tâches sans intervention humaine dans des environnements extrêmement variés. Les fautes de tels systèmes peuvent avoir des conséquences inacceptables vis à vis de la sûreté de fonctionnement, des performances ou de la mission. Le test en simulation de tels systèmes est efficace pour révéler et éliminer ces fautes tout en présentant l'avantage d'être moins coûteux, moins dangereux et potentiellement plus exhaustif qu'un test dans le monde réel. L'objectif de nos travaux est de trouver comment caractériser le domaine d'entrée du test, d'identifier les critères de sélection à retenir pour les tests, d'élucider comment satisfaire ces critères en combinant des procédés de génération de tests classiques et des procédés de génération de mondes et ainsi, de proposer une approche permettant de définir et de réaliser les tests dans le contexte des systèmes autonomes. Pour cela, nous avons tout d'abord identifié divers composants qui interviennent durant les phases de tests que sont la génération des entrées, l'exécution du test, ainsi que l'analyse des résultats de l'exécution. Nous utilisons le simulateur Morse qui est générique et basé sur le moteur de rendu 3D \textit{Blender Game engine} et qui permet de simuler un ensemble de capteurs et d’actionneurs. Le système sous test comprend les modules robotiques nécessaires au service de navigation, générés à partir de modèles GenoM. Nous avons mené une première expérience dans le but d'observer l'indéterminisme des modules dédiés à la navigation.

National audience; Autonomous robots are mainly tested through field experiments. This approach is costly and may present risks. An alternative method is to perform part of the tests on a simulation platform. This raises several challenges : the generation of complex virtual environments, the automated verification of the observed behavior (test oracle), and the imperfect fidelity of the simulation compared to real field tests. This thesis is divided into two parts centered around these challenges.In a first part, our work addresses these different points through the case study of an agricultural robot, the Oz robot from Naïo Technologies. In particular, we make a comparative analysis of the faults found in simulation and in the field. The main contribution of this part is to demonstrate the feasibility and efficiency of simulation testing of an industrial case. Despite their imperfect fidelity, the simulation tests reveal most of the faults found by the experiments with the real robot, including the one that caused the majority of the failures in the field. They also reveal a new fault that was unnoticed in the field but later confirmed by the industry. However, the implementation effort of the virtual tests is important, with in particular thedevelopment of a data generator specific to the 3D environments of the robot. This observation led the continuation of our work towards the study of test generation.The second part of our work introduces a new test generation method and a prototype that implements it. It is based on a purely declarative data model, combining SMT constraint resolution and random sampling. Although the starting point of this work is the generation of virtual environments for autonomous systems, our generation method applies to a much broader domain. It allows the generation of structured data of varying sizes, while respecting semantic properties and providing diversity. We have evaluated our method on four case studies coming from various application domains (the Oz robot, a management system for taxation, color gradient images and tree structures). Our results show that data are generated efficiently and cover the solution space. Our method is competitive with the existing approaches to which we compared it.; Les robots autonomes sont principalement testés par des expérimentations sur le terrain. Cette approche est coûteuse et peut présenter des risques. Une méthode alternative consiste à réaliser une partie des tests sur une plate-forme de simulation. Ceci soulève plusieurs défis : la génération d’environnements virtuels complexes, la vérification automatisée du comportement observé (oracle de test), et la fidélité imparfaite de la simulation par rapport à des tests sur le terrain. Cette thèse estdivisée en deux parties axées autour de ces problématiques.Dans une première partie, nos travaux abordent ces différents points au travers du cas d’étude d’un robot agricole, le robot Oz de la société Naïo Technologies. Nous faisons en particulier une analyse comparative des fautes trouvées en simulation et sur le terrain. La contribution principale de cette partie est de démontrer la faisabilité et l’efficacité du test en simulation sur un cas industriel. Malgré leur fidélité imparfaite, les tests en simulation révèlent la plupart des fautes trouvées par les expérimentations avec le robot réel, y compris celles ayant causé la majorité desdéfaillances sur le terrain. Ils révèlent également une nouvelle faute passée inaperçue sur le terrain mais confirmée par l’industriel. Cependant, l’effort d’implémentation des tests virtuels se révèle important, avec notamment le développement d’un générateur de données spécifiques aux environnements 3D du robot. Ce constat a mené la suite de nos travaux vers l’étude de la génération de tests.La deuxième partie de nos travaux introduit une nouvelle méthode de génération de test et un outil qui l’implémente. Elle se base sur un modèle dedonnées purement déclaratif, en combinant la résolution de contraintes SMT et l’échantillonnage aléatoire. Bien que le point de départ de ces travaux soit la génération d’environnements virtuels pour les systèmes autonomes, notre méthode de génération s’applique à un domaine bien plus large. Elle permet de produire des données structurées de tailles variables, tout en respectant des propriétés sémantiques et en offrant de la diversité. Nous avons évalué notre méthode sur quatre cas d’étude venant de domaines d’application variés (le robot Oz, un système de gestion de taxe, des images de dégradé de gris et des structures arborescentes). Nos résultats montrent des données générées efficacement et couvrant bien l’espace des solutions. Notre méthode est compétitive au regard des approches existantesauxquelles nous l’avons comparée.

Autonomous robots are mainly tested through field experiments. This approach is costly and may present risks. An alternative method is to perform part of the tests on a simulation platform. This raises several challenges : the generation of complex virtual environments, the automated verification of the observed behavior (test oracle), and the imperfect fidelity of the simulation compared to real field tests. This thesis is divided into two parts centered around these challenges. In a first part, our work addresses these different points through the case study of an agricultural robot, the Oz robot from Naïo Technologies. In particular, we make a comparative analysis of the faults found in simulation and in the field. The main contribution of this part is to demonstrate the feasibility and efficiency of simulation testing of an industrial case. Despite their imperfect fidelity, the simulation tests reveal most of the faults found by the experiments with the real robot, including the one that caused the majority of the failures in the field. They also reveal a new fault that was unnoticed in the field but later confirmed by the industry. However, the implementation effort of the virtual tests is important, with in particular the development of a data generator specific to the 3D environments of the robot. This observation led the continuation of our work towards the study of test generation. The second part of our work introduces a new test generation method and a prototype that implements it. It is based on a purely declarative data model, combining SMT constraint resolution and random sampling. Although the starting point of this work is the generation of virtual environments for autonomous systems, our generation method applies to a much broader domain. It allows the generation of structured data of varying sizes, while respecting semantic properties and providing diversity. We have evaluated our method on four case studies coming from various application domains (the Oz robot, a management system for taxation, color gradient images and tree structures). Our results show that data are generated efficiently and cover the solution space. Our method is competitive with the existing approaches to which we compared it., Les robots autonomes sont principalement testés par des expérimentations sur le terrain. Cette approche est coûteuse et peut présenter des risques. Une méthode alternative consiste à réaliser une partie des tests sur une plate-forme de simulation. Ceci soulève plusieurs défis : la génération d’environnements virtuels complexes, la vérification automatisée du comportement observé (oracle de test), et la fidélité imparfaite de la simulation par rapport à des tests sur le terrain. Cette thèse est divisée en deux parties axées autour de ces problématiques. Dans une première partie, nos travaux abordent ces différents points au travers du cas d’étude d’un robot agricole, le robot Oz de la société Naïo Technologies. Nous faisons en particulier une analyse comparative des fautes trouvées en simulation et sur le terrain. La contribution principale de cette partie est de démontrer la faisabilité et l’efficacité du test en simulation sur un cas industriel. Malgré leur fidélité imparfaite, les tests en simulation révèlent la plupart des fautes trouvées par les expérimentations avec le robot réel, y compris celles ayant causé la majorité des défaillances sur le terrain. Ils révèlent également une nouvelle faute passée inaperçue sur le terrain mais confirmée par l’industriel. Cependant, l’effort d’implémentation des tests virtuels se révèle important, avec notamment le développement d’un générateur de données spécifiques aux environnements 3D du robot. Ce constat a mené la suite de nos travaux vers l’étude de la génération de tests. La deuxième partie de nos travaux introduit une nouvelle méthode de génération de test et un outil qui l’implémente. Elle se base sur un modèle de données purement déclaratif, en combinant la résolution de contraintes SMT et l’échantillonnage aléatoire. Bien que le point de départ de ces travaux soit la génération d’environnements virtuels pour les systèmes autonomes, notre méthode de génération s’applique à un domaine bien plus large. Elle permet de produire des données structurées de tailles variables, tout en respectant des propriétés sémantiques et en offrant de la diversité. Nous avons évalué notre méthode sur quatre cas d’étude venant de domaines d’application variés (le robot Oz, un système de gestion de taxe, des images de dégradé de gris et des structures arborescentes). Nos résultats montrent des données générées efficacement et couvrant bien l’espace des solutions. Notre méthode est compétitive au regard des approches existantes auxquelles nous l’avons comparée.

One of the major challenges for the deployment of autonomous systems in diverse, unstructured and human shared environments, is the trust that can be placed in those systems. Indeed, internal faults in those systems, uncertainties on the perception, or even unforeseen situations, threat this confidence. Our work focus in autonomous robots, which are part of autonomous systems. The validation of the navigation software embedded in robots typically involves test campaigns in the field, which are expensive and potentially risky for the robot itself or its environment. These tests are able to test the system only in a small subset of situations. An alternative is to perform simulation-based testing, by immersing the software in virtual worlds. The aim of this thesis is to study the possibilities and limits offered by simulation-based testing of embedded software in autonomous systems. Our work deals particularly with simulation-based testing of the navigation layer of autonomous mobile robots. The first chapter introduce the contexts of dependability, autonomous systems and their testing, simulation and procedural generation of worlds. We identify and discuss the issues related to autonomous systems simulation-based testing, such as the definition and generation of inputs as well as the oracle. The procedural generation of worlds used in video games is retained as a way to answer the problem of the generation of test inputs (worlds and missions). A first contribution is presented in the second chapter, which is based on the definition and implementation of a first experimental simulation-based testing framework with a mobile robot. The navigation software used is integrated into the Genom framework and tested with the MORSE simulator. Through this experiment, first conclusions are drawn on the relevance of the procedural generation of worlds, and on the oracle to be considered. Measures such as tortuousness or indeterminism of navigation are defined. This first work also leads to propose an approach to define levels of difficulty of worlds. The purpose of the third chapter is to identify whether faults known and corrected in a academic navigation software could have been detected through simulation-based testing. Nearly 10 years of commits of the navigation software (including the P3D module which is an academic version of a trajectory planner used by NASA) were thus analyzed. Each fault detected is studied to determine the oracle necessary to detect it whether it could be activated in simulation. Many recommendations are extracted from this study, especially on the properties of the oracle to set up for this type of system. In the fourth chapter, lessons learned from the previous two chapters are implemented for the case of an industrial robot. The considered system, provided by our industrial partner Naïo is the agricultural robot Oz. The conclusions of the preceding chapters regarding the world generation and the oracles are validated by an intensive test campaign in simulation.; Un des défis majeurs pour le déploiement de systèmes autonomes dans des environnements variés, non structurés et à proximité de l'homme, est d'établir la confiance entre ces systèmes et leurs utilisateurs. En effet, les fautes internes du système, les incertitudes sur la perception, ou encore les situations non prévues, sont des menaces importantes qui pèsent sur cette confiance. Nos travaux se concentrent sur les robots autonomes qui font partis des systèmes autonomes. La validation du logiciel de navigation embarqué dans les robots est généralement centrée sur des tests sur le terrain, qui sont coûteux et potentiellement risqués pour le robot lui-même ou son environnement. De plus, il n'est possible de tester le système que dans un sous-ensemble restreint de situations. Une approche alternative consiste à effectuer des tests basés sur la simulation en immergeant le logiciel dans des mondes virtuels. L'objectif de cette thèse est d'étudier les possibilités et les limites qu'offre le test en simulation du logiciel embarqué dans les systèmes autonomes. Nos travaux traitent particulièrement du test en simulation de la couche de navigation de systèmes autonomes mobiles. Le premier chapitre présente les contextes de la sûreté de fonctionnement, des systèmes autonomes et de leur test, de la simulation et de la génération procédurale de mondes. Les problématiques liées au test des systèmes autonomes en simulation, telles que la définition et la génération des entrées ainsi que l'expression de l'oracle, sont identifiées et discutées. La génération procédurale de mondes utilisée dans les jeux vidéos est retenue comme piste pour répondre au problème de la générations des entrées de test (mondes et missions). Une première contribution est proposée dans le 2ème chapitre qui s'appuie sur la définition et l'implémentation d'une première plateforme expérimentale de test en simulation avec un robot mobile. Le logiciel de navigation utilisé est intégré dans le framework Genom et testé avec le simulateur MORSE. À travers cette expérimentation, des premières conclusions sont établies sur la pertinence de la génération procédurale de mondes, et sur l'oracle à considérer. Des mesures comme la tortuosité ou l'indéterminisme de la navigation sont définies. Ce premier travail mène également à proposer une approche permettant de définir des niveaux de difficulté de mondes. L'objectif du 3ème chapitre est d'identifier si les fautes connues et corrigées dans un logiciel de navigation auraient pu être détectées via la simulation. Près de 10 ans de commits du logiciel de navigation (dont le module P3D qui est une version académique d'un planificateur de trajectoire utilisé par la NASA) ont été ainsi analysés. Chaque faute relevée est étudiée pour déterminer si elle serait activable en simulation, et l'oracle nécessaire pour la détecter. De nombreuses recommandations sont extraites de cette étude, notamment sur les propriétés de l'oracle à mettre en place pour ce genre de système. Dans le quatrième chapitre, les enseignements tirés des deux chapitres précédents sont mis en œuvre dans une étude de cas d'un robot industriel. Le système considéré, fourni par notre partenaire industriel Naïo est celui du robot agricole bineur Oz. Les conclusions des chapitres précédents concernant la génération de monde et les oracles nécessaires sont validées par une campagne de test intensifs en simulation.

National audience; One of the major challenges for the deployment of autonomous systems in diverse, unstructured and human shared environments, is the trust that can be placed in those systems. Indeed, internal faults in those systems, uncertainties on the perception, or even unforeseen situations, threat this confidence. Our work focus in autonomous robots, which are part of autonomous systems. The validation of the navigation software embedded in robots typically involves test campaigns in the field, which are expensive and potentially risky for the robot itself or its environment. These tests are able to test the system only in a small subset of situations. An alternative is to perform simulation-based testing, by immersing the software in virtual worlds. The aim of this thesis is to study the possibilities and limits offered by simulation-based testing of embedded software in autonomous systems. Our work deals particularly with simulation-based testing of the navigation layer of autonomous mobile robots. The first chapter introduce the contexts of dependability, autonomous systems and their testing, simulation and procedural generation of worlds. We identify and discuss the issues related to autonomous systems simulation-based testing, such as the definition and generation of inputs as well as the oracle. The procedural generation of worlds used in video games is retained as a way to answer the problem of the generation of test inputs (worlds and missions). A first contribution is presented in the second chapter, which is based on the definition and implementation of a first experimental simulation-based testing framework with a mobile robot. The navigation software used is integrated into the Genom framework and tested with the MORSE simulator. Through this experiment, first conclusions are drawn on the relevance of the procedural generation of worlds, and on the oracle to be considered. Measures such as tortuousness or indeterminism of navigation are defined. This first work also leads to propose an approach to define levels of difficulty of worlds. The purpose of the third chapter is to identify whether faults known and corrected in a academic navigation software could have been detected through simulation-based testing. Nearly 10 years of commits of the navigation software (including the P3D module which is an academic version of a trajectory planner used by NASA) were thus analyzed. Each fault detected is studied to determine the oracle necessary to detect it whether it could be activated in simulation. Many recommendations are extracted from this study, especially on the properties of the oracle to set up for this type of system. In the fourth chapter, lessons learned from the previous two chapters are implemented for the case of an industrial robot. The considered system, provided by our industrial partner Naïo is the agricultural robot Oz. The conclusions of the preceding chapters regarding the world generation and the oracles are validated by an intensive test campaign in simulation.; Un des défis majeurs pour le déploiement de systèmes autonomes dans des environnements variés, non structurés et à proximité de l’homme, est d’établir la confiance entre ces systèmes et leurs utilisateurs. En effet, les fautes internes du système, les incertitudes sur la perception, ou encore les situations non prévues, sont des menaces importantes qui pèsent sur cette confiance. Nos travaux se concentrent sur les robots autonomes qui font partis des systèmes autonomes. La validation du logiciel de navigation embarqué dans les robots est généralement centrée sur des tests sur le terrain, qui sont coûteux et potentiellement risqués pour le robot lui-même ou son environnement. De plus, il n’est possible de tester le système que dans un sous-ensemble restreint de situations. Une approche alternative consiste à effectuer des tests basés sur la simulation en immergeant le logiciel dans des mondes virtuels. L’objectif de cette thèse est d’étudier les possibilités et les limites qu’offre le test en simulation du logiciel embarqué dans les systèmes autonomes. Nos travaux traitent particulièrement du test en simulation de la couche de navigation de systèmes autonomes mobiles. Le premier chapitre présente les contextes de la sûreté de fonctionnement, des systèmes autonomes et de leur test, de la simulation et de la génération procédurale de mondes. Les problématiques liées au test des systèmes autonomes en simulation, telles que la définition et la génération des entrées ainsi que l’expression de l’oracle, sont identifiées et discutées. La génération procédurale de mondes utilisée dans les jeux vidéos est retenue comme piste pour répondre au problème de la générations des entrées de test (mondes et missions). Une première contribution est proposée dans le 2e chapitre qui s’appuie sur la définition et l’implémentation d’une première plateforme expérimentale de test en simulation avec un robot mobile. Le logiciel de navigation utilisé est intégré dans le framework Genom et testé avec le simulateur MORSE. À travers cette expérimentation, des premières conclusions sont établies sur la pertinence de la génération procédurale de mondes, et sur l’oracle à considérer. Des mesures comme la tortuosité ou l’indéterminisme de la navigation sont définies. Ce premier travail mène également à proposer une approche permettant de définir des niveaux de difficulté de mondes. L’objectif du 3e chapitre est d’identifier si les fautes connues et corrigées dans un logiciel de navigation auraient pu être détectées via la simulation. Près de 10 ans de commits du logiciel de navigation (dont le module P3D qui est une version académique d’un planificateur de trajectoire utilisé par la NASA) ont été ainsi analysés. Chaque faute relevée est étudiée pour déterminer si elle serait activable en simulation, et l’oracle nécessaire pour la détecter. De nombreuses recommandations sont extraites de cette étude, notamment sur les propriétés de l’oracle à mettre en place pour ce genre de système. Dans le quatrième chapitre, les enseignements tirés des deux chapitres précédents sont mis en oeuvre dans une étude de cas d’un robot industriel. Le système considéré, fourni par notre partenaire industriel Naïo est celui du robot agricole bineur Oz. Les conclusions des chapitres précédents concernant la génération de monde et les oracles nécessaires sont validées par une campagne de test intensifs en simulation.

The main objective of this thesis is to contribute to elaborating a mobile system test method. The proposed approach is based on test definition using scenarios and their verification on an execution trace. A scenario modelizes the behavior and the interactions we want to achieve on a set of nodes. Considering the characteristics of mobile systems we represented scenarios from two different but complementary points of view. The first represents communication events between nodes and the second represents the link topology between the nodes. Our approach is composed of two steps : a first step to specify the test cases by using scenarios and a second step to verify these scenarios on execution flows. The first step consists in using the dedicated TERMOS language in order to specify the test cases of the mobile application. The TERMOS language has been developed in the UML Papyrus workshop. Based on the graphically defined scenarios, we generate an automaton for each one of them, as well as a sequence of topologies which we will be using in the next step. The second step consists in verifying each scenario by using execution traces from the application to be tested. Therefore a first tool detects scenario topology sequences in the execution flow. For each one of them the automaton is executed and comes out with a verdict. The analysis of all the verdicts of a scenario allows the detection of faults in the system.; L'objectif de cette thèse est de contribuer à l'élaboration d'une méthode de test de systèmes mobiles. L'approche développée est fondée sur la description de tests à l'aide de scénarios et leurs vérifications sur une trace d'exécution. Un scénario modélise le comportement et les interactions que l'on souhaite observer entre un ensemble de nœuds. Les caractéristiques des systèmes mobiles nous ont conduit à représenter un scénario sous deux points de vue différents et complémentaires. Un premier représente des événements de communications entre les nœuds et un second représente la topologie des liens entre ces nœuds. Notre approche est décomposée en deux étapes : une étape de spécification des cas de tests à l'aide de scénarios et une étape de vérification de ces scénarios sur des traces d'exécutions. La première consiste à spécifier à l'aide du langage dédié TERMOS les cas de test de l'application mobile à vérifier. Ce langage TERMOS a été mis en œuvre au sein de l'atelier UML Papyrus. À partir des scénarios décrits de manière graphique, nous générons pour chacun d'eux un automate ainsi qu'une séquence de topologie que nous utilisons dans l'étape suivante. La deuxième étape consiste à vérifier chaque scénario sur des traces d'exécutions provenant de l'application à tester. Pour cela un premier outil recherche les occurrences de la séquence de topologie du scénario dans la trace d'exécution. Pour chacune d'entre elles, l'automate est exécuté et conclut à un verdict. L'analyse de l'ensemble des verdicts d'un scénario permet de détecter les fautes présentes dans le système.

The main objective of this thesis is to contribute to elaborating a mobile system test method. The proposed approach is based on test definition using scenarios and their verification on an execution trace. A scenario modelizes the behavior and the interactions we want to achieve on a set of nodes. Considering the characteristics of mobile systems we represented scenarios from two different but complementary points of view. The first represents communication events between nodes and the second represents the link topology between the nodes. Our approach is composed of two steps : a first step to specify the test cases by using scenarios and a second step to verify these scenarios on execution flows. The first step consists in using the dedicated TERMOS language in order to specify the test cases of the mobile application. The TERMOS language has been developed in the UML Papyrus workshop. Based on the graphically defined scenarios, we generate an automaton for each one of them, as well as a sequence of topologies which we will be using in the next step. The second step consists in verifying each scenario by using execution traces from the application to be tested. Therefore a first tool detects scenario topology sequences in the execution flow. For each one of them the automaton is executed and comes out with a verdict. The analysis of all the verdicts of a scenario allows the detection of faults in the system.; L'objectif de cette thèse est de contribuer à l'élaboration d'une méthode de test de systèmes mobiles. L'approche développée est fondée sur la description de tests à l'aide de scénarios et leurs vérifications sur une trace d'exécution. Un scénario modélise le comportement et les interactions que l'on souhaite observer entre un ensemble de nœuds. Les caractéristiques des systèmes mobiles nous ont conduit à représenter un scénario sous deux points de vue différents et complémentaires. Un premier représente des événements de communications entre les nœuds et un second représente la topologie des liens entre ces nœuds. Notre approche est décomposée en deux étapes : une étape de spécification des cas de tests à l'aide de scénarios et une étape de vérification de ces scénarios sur des traces d'exécutions. La première consiste à spécifier à l'aide du langage dédié TERMOS les cas de test de l'application mobile à vérifier. Ce langage TERMOS a été mis en œuvre au sein de l'atelier UML Papyrus. À partir des scénarios décrits de manière graphique, nous générons pour chacun d'eux un automate ainsi qu'une séquence de topologie que nous utilisons dans l'étape suivante. La deuxième étape consiste à vérifier chaque scénario sur des traces d'exécutions provenant de l'application à tester. Pour cela un premier outil recherche les occurrences de la séquence de topologie du scénario dans la trace d'exécution. Pour chacune d'entre elles, l'automate est exécuté et conclut à un verdict. L'analyse de l'ensemble des verdicts d'un scénario permet de détecter les fautes présentes dans le système.

Autonomous systems operating in the vicinity of humans are critical in that they potentially harm humans. In these systems, fault removal is not sufficient given the command complexity and their interactions with an unstructured environment. By a fault tolerance approach, we consider a safety monitor separated from the main command and able to observe and intervene on the system. The monitor behavior is specified by safety rules that must both ensure safety and permit the system to carry out its tasks in absence of hazard. We propose a systematic method to obtain these safety rules. The hazards, determined by a risk analysis, are formally modeled, then an algorithm synthesizes safe and permissive rules, if any exists. The method is tooled both for modeling and synthesis by use of the model-checker NuSMV. Method and tools are applied to the industrial use case of a robotic co-worker.; Les systèmes autonomes, notamment ceux opérant à proximité d'êtres humains, soulèvent des problèmes de sécurité-innocuité puisqu'ils peuvent causer des blessures. La complexité de la commande de ces systèmes, ainsi que leurs interactions avec un environnement peu structuré, rendent difficile l'élimination complète des fautes. Nous adoptons donc une démarche de tolérance aux fautes en considérant un moniteur de sécurité séparé de la commande principale et qui dispose de ses propres moyens d'observation et d'intervention. Le comportement de ce moniteur est régi par des règles qui doivent assurer la sécurité du système tout en lui permettant de remplir ses fonctions. Nous proposons une méthode systématique pour obtenir ces règles de sécurité. Les dangers, déterminés par une analyse de risque, sont modélisés formellement puis un algorithme synthétise des règles sûres et permissives, s'il en existe. Nous avons outillé cette méthode pour les étapes de modélisation et de synthèse en nous appuyant sur l'outil de vérification de modèle NuSMV. L'étude d'un cas industriel illustre l'application de la méthode et des outils sur un robot manufacturier dans un environnement humain.

Autonomous systems operating in the vicinity of humans are critical in that they potentially harm humans. In these systems, fault removal is not sufficient given the command complexity and their interactions with an unstructured environment. By a fault tolerance approach, we consider a safety monitor separated from the main command and able to observe and intervene on the system. The monitor behavior is specified by safety rules that must both ensure safety and permit the system to carry out its tasks in absence of hazard. We propose a systematic method to obtain these safety rules. The hazards, determined by a risk analysis, are formally modeled, then an algorithm synthesizes safe and permissive rules, if any exists. The method is tooled both for modeling and synthesis by use of the model-checker NuSMV. Method and tools are applied to the industrial use case of a robotic co-worker.; Les systèmes autonomes, notamment ceux opérant à proximité d'êtres humains, soulèvent des problèmes de sécurité-innocuité puisqu'ils peuvent causer des blessures. La complexité de la commande de ces systèmes, ainsi que leurs interactions avec un environnement peu structuré, rendent difficile l'élimination complète des fautes. Nous adoptons donc une démarche de tolérance aux fautes en considérant un moniteur de sécurité séparé de la commande principale et qui dispose de ses propres moyens d'observation et d'intervention. Le comportement de ce moniteur est régi par des règles qui doivent assurer la sécurité du système tout en lui permettant de remplir ses fonctions. Nous proposons une méthode systématique pour obtenir ces règles de sécurité. Les dangers, déterminés par une analyse de risque, sont modélisés formellement puis un algorithme synthétise des règles sûres et permissives, s'il en existe. Nous avons outillé cette méthode pour les étapes de modélisation et de synthèse en nous appuyant sur l'outil de vérification de modèle NuSMV. L'étude d'un cas industriel illustre l'application de la méthode et des outils sur un robot manufacturier dans un environnement humain.