Cette thèse se situe dans la problématique de la conduite en convoi de véhicules autonomes : des ensembles de véhicules qui se déplacent en conservant une configuration spatiale, sans aucune accroche matérielle. Ses objectifs sont d'abord, la définition d'une approche de prise de décision pour les systèmes de convois de véhicules, puis, la définition d'une approche de vérification, adaptée à la preuve de propriétés relatives aux convois de véhicules, avec une attention particulière envers les propriétés de sûreté.L'approche pour la prise de décision est décentralisée et auto organisée : chaque véhicule détermine son comportement de façon locale, à partir de ses propres capacités de perception, sans avoir recours à une communication explicite, de telle sorte que l'organisation du convoi, son maintien et son évolution soient le résultat émergeant du comportement de chaque véhicule. L'approche proposée s'applique a des convois suivant plusieurs types de configuration, et permet des changements dynamiques de configuration.L'approche proposée pour la vérification de propriétés de sûreté des convois de véhicules, adopte le model-checking comme technique de preuve. Pour contourner le problème de l'explosion combinatoire, rencontré dans la vérification des systèmes complexes, nous avons proposé une méthode compositionnelle de vérification, qui consiste a décomposer le système en sous systèmes et à associer une propriété auxiliaire à chacun des sous systèmes. La propriété globale sera ensuite déduite de l'ensemble des propriétés auxiliaires, par l'application d'une règle de déduction compositionnelle. La complexité calculatoire est mieux maîtrisée car le model-checking s'applique aux sous-systèmes. Nous proposons une règle de déduction adaptée aux systèmes de conduite en convoi, en particulier ceux qui sont basés sur des approches décentralisées. La règle considère chaque véhicule comme un composant. Elle est consistante sous la condition que l'ajout d'un nouveau composant au système n'a pas d'influence sur le comportement du reste du système. L'approche décentralisée proposée pour la conduite en convoi satisfait cette condition. Deux propriétés de sûreté ont été vérifiées : absence de collision et évolution confortable pour les passagers / This thesis places in the framework of Platoons, sets of autonomous vehicles that move together while keeping a spatial configuration, without any material coupling. Goals of the thesis are: first, the definition of a decision making approach for platoon systems. Second, the definition of a method for the verification of safety properties associated to the platoon system.The proposed decision making approach is decentralized and self-organized. Platoon vehicles are autonomous, they act based only on their perception capabilities. The configuration emerges as a result of the individual behavior of each of the platoon vehicle. The proposed approach can be applied to platoon with different configurations, and allows for dynamic change of configuration.The proposed verification method uses the model-checking technique. Model checking of complex system can lead to the combinatory explosion problem. To deal with this problem, we choose to use a compositional verification method. Compositional methods decompose system models into different components and associate to each component an auxiliary property. The global property can then be deduced from the set of all the auxiliary properties, by applying a compositional deduction rule. We define a deduction rule suitable for decentralised platoon systems. The deduction rule considers each vehicle as a component. It is applicable under the assumption that adding a new component to an instance of the system does not modify behavior of the instance. Two safety properties have been verified : collision avoidance.

Nous étudions le problème de la synthèse automatique de programmes dans des architectures multi-composants tels qu'elles respectent les spécifications par construction. Le principal objectif de cette thèse est de développer des procédures pour résoudre le problème de synthèse qui peut conduire à des implémentations efficaces. Chaque composant a une observation partielle sur l'état global du système multi-composants. Le problème est alors de fournir des protocoles basés sur les observations tel que les composants synthétisés assurent les spécifications pour tout le comportement de leur environnement.L'environnement peut être antagoniste, ou peut avoir ses propres objectifs et se comporter de façon rationnelle. Nous étudions d'abord le problème de synthèse lorsque l'environnement est présumé antagoniste. Pour ce contexte, nous proposons une procédure "Safraless" pour la synthèse d'un composant partiellement informé et un environnement omniscient à partir de spécifications KLTL+. Elle est implémentée dans l'outil Acacia-K. Ensuite, nous étudions le problème de synthèse lorsque les composants de l'environnement ont leurs propres objectifs et sont rationnels. Pour le cadre plus simple de l'information parfaite, nous fournissons des complexités serrées pour des objectifs oméga-réguliers particuliers. Pour le cas de l'information imparfaite, nous prouvons que le problème de la synthèse rationnelle est indécidable en général, mais nous regagnons la décidabilité si on demande à synthétiser un composant avec observation partielle contre un environnement multi-composante, omniscient et rationnel. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished

Nous nous intéressons aux approches formelles pour le développement de systèmes réactifs critiques. Le langage synchrone Lustre pour la spécification de tels systèmes a subit des évolutions majeurs au cours des dernières années en intégrant dans sa sémantique à base flots de données synchrones des constructions de plus haut-niveau appelées automates de modes (dans le langage Scade 6). Ceux-ci mettent en œuvre l'activation de modes de calculs en fonction des états et des transitions de l'automate, et reposent pour cela sur la sémantique des horloges du langage Lustre. En particulier, nous étudiions la prise en compte des horloges et des automates de modes dans l'outil de génération de tests GATeL dédié à l'origine au langage Lustre mono-horloge (flots de données purs). GATeL génère automatiquement des séquences de tests pour un modèle à partir d'un objectif de test décrit en Lustre à travers une exploration en arrière des dépendances entre flots et selon des teniques de résolution de contraintes. Nous présentons ces différents domaines et la mise en oeuvre des modifications apportées à l'outil pour prendre en compte les automates de modes. Enfin, nous définissons des critères de couverture structurelle pour les automates de modes et montrons alors comment, en les traduisant de manière automatique sous forme d'objectifs de tests, GATeL permet de générer des séquences couvrant ces critères.

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

Dans cette thèse, nous étudions les systèmes de transitions asynchrones en tant que modèles pour la sémantique des systèmes réactifs. Les systèmes de transitions asynchrones (STA) de Shields et Bednarczyk, sont une généralisation des systèmes de transitions (ST) et des structures d'événements stables (SE). Tout d'abord nous définissons l'opération de raffinement d'actions sur les STA, qui permet de relier entre elles les descriptions d'un système a différents niveaux d'abstraction. Ensuite, nous proposons des équivalences sémantiques sur les STA et nous étudions leur compatibilité avec l'opération de raffinement. Enfin, nous relions notre cadre avec celui de la théorie des sémantiques opérationnelles structurées (SOS) de Plotkin

Notre thèse se situe dans le domaine des méthodes formelles appliquées aux systèmes réactifs. Nous modélisons et traitons ces systèmes, en continuelle interaction avec leur environnement, grâce au langage<br />synchrone Lustre.<br /><br />D'abord, sur la base d'un travail précurseur, nous établissons pour Lustre une méthode de preuve inductive des propriétés de sûreté. Cette méthode est optimisée, afin de prendre en compte au mieux la dynamique des systèmes. Elle est implémentée dans un outil de preuve, Gloups.<br /><br />Ensuite, suivant le modèle de la méthode B, nous définissons un calcul de raffinement pour Lustre. Ce calcul est à la fois adapté à Lustre et exprimé en ce langage. Les obligations de preuve qui assurent la<br />correction du raffinement peuvent être traitées par Gloups. Pour faciliter le développement, un autre outil, Flush, génère automatiquement les obligations pour Gloups.<br /><br />Ainsi, nous utilisons Lustre à la fois comme langage de programmation et comme cadre formel d'un développement maîtrisé. L'intérêt de ce<br />procédé réside dans la simplicité du langage et dans son adaptation aux systèmes réactifs : en ce domaine, notre méthode de raffinement est suffisamment expressive, sans être inutilement compliquée. Des exemples viennent démontrer l'intérêt de la méthode.

Un robot mobile autonome doit réaliser des tâches non répétitives dans un environnement imparfaitement connu et non-coopératif, voire hostile. Dans ce contexte les missions attribuées au robot ne peuvent être définies que de façon abstraite et peu détaillée, et le robot doit être doté de moyens pour les interpréter, appréhender l'environnement, décider des actions adéquates et réagir aux événements asynchrones. Afin de concilier décision et réaction, l'architecture de contrôle proposée, c'est-à-dire la manière dont sont organisées les composantes logicielles du robot, comporte deux niveaux hiérarchiques : les niveaux décisionnel et fonctionnel. Ce second niveau, objet principal de la thèse, fournit l'ensemble des capacités opératoires du système (perception, modélisation, mouvements et actions). La première partie du mémoire présente l'architecture globale et fournit un état de l'art et une analyse critique focalisée sur l'organisation des systèmes réactifs. La seconde partie explicite les conditions requises au niveau de la couche fonctionnelle pour satisfaire l'autonomie, la réactivité et la programmabilité du robot. Ces caractéristiques, associées à la grande diversité et aux contraintes temporelles des fonctions opératoires, ont conduit à une structuration en modules. La formalisation structurelle, comportementale et fonctionnelle des modules a permis en particulier de concevoir des méthodes générales d'intégration de fonctions. Les fonctions ainsi encapsulées dans les modules composent un ensemble de services homogènes, réactifs et observables à la disposition du niveau décisionnel qui accomplit les tâches du robot en les combinant dynamiquement en un arbre d'activités. Les modules sont décrits et produits au moyen d'un langage de spécification associé à un générateur automatique nommé GenoM. La dernière partie présente trois intégrations complètes. La première concerne Hilare, un robot expérimental d'intérieur é quipé de nombreux capteurs et fonctionnalités. Des méthodes originales de localisation et de contrôle de déplacement pour véhicule non-holonome sont détaillées. La seconde porte sur la navigation en milieu naturel du robot tout terrain ADAM. La dernière, relative à la coopération multi-robots, a conduit à une simulation réaliste d'une quinzaine de robots (sous UNIX) et à une expérimentation réelle avec trois robots Hilare (sous VxWorks).

Nous nous intéressons aux approches formelles pour le développement de systèmes réactifs critiques. Le langage synchrone Lustre pour la spécification de tels systèmes a subit des évolutions majeurs au cours des dernières années en intégrant dans sa sémantique à base flots de données synchrones des constructions de plus haut-niveau appelées automates de modes (dans le langage Scade 6). Ceux-ci mettent en œuvre l’activation de modes de calculs en fonction des états et des transitions de l’automate, et reposent pour cela sur la sémantique des horloges du langage Lustre. En particulier, nous étudiions la prise en compte des horloges et des automates de modes dans l’outil de génération de tests GATeL dédié à l’origine au langage Lustre mono-horloge (flots de données purs). GATeL génère automatiquement des séquences de tests pour un modèle à partir d’un objectif de test décrit en Lustre à travers une exploration en arrière des dépendances entre flots et selon des teniques de résolution de contraintes. Nous présentons ces différents domaines et la mise en oeuvre des modifications apportées à l’outil pour prendre en compte les automates de modes. Enfin, nous définissons des critères de couverture structurelle pour les automates de modes et montrons alors comment, en les traduisant de manière automatique sous forme d’objectifs de tests, GATeL permet de générer des séquences couvrant ces critères. / Lustre is a synchronous dataflow-oriented language for the specification of reactive systems. Since its definition, it has been extended to support mode automata, a formalism in which computation modes are activated according to an extended state-machine. The semantics of mode-automata is heavily based on an appropriate use of the clock sampling features of Lustre. We present the modifications made in GATeL, an automatic test sequences generator originally designed for a mono-rate subset of Lustre. GATeL performs a lazy goal-oriented test sequences generation, based on constraint logic programming. We modify it so that it can handle the temporal constraints of clocks internally and efficiently generate tests sequences from state-maines specifications. We also present some existing structural test criteria for state-machines and adapt them to the specific case of mode-automata.

Le comportement de deux matériaux réactifs, une formulation élastomère de caoutchouc naturel et un système thermodurcissable polyuréthane (PU), est étudié pour être modélisé. De nombreuses méthodologies sont mises au point dans ce travail pour améliorer les mesures. La cinétique réactionnelle du PU est suivie par calorimétrie différentielle (DSC) et par titrage chimique. L'analyse isoconversionnelle met en évidence trois réactions chimiques formant un réseau tridimensionnel. Le modèle cinétique met en série trois modèles de Piloyan. La cinétique du caoutchouc naturel est suivie par rhéomètrie, par DSC et par gonflement. Le modèle d'Isayev, très simple, donne des résultats satisfaisants mais ignore la réversion. Le modèle de Coran Ding et Leonov, ayant de nombreux paramètres, donne de très bons résultats. La rhéologie est ensuite étudiée. Pour le PU, le couplage cinétique-rhéologie est nécessaire et conduit à une étude rhéocinétique. Le modèle de Castro et Macosko est utilisé. Le caoutchouc naturel, non réactif durant le remplissage, permet de découpler cinétique et rhéologie. Le modèle de Carreau Yasuda est alors utilisé. Le glissement à la paroi est étudié avec la méthode de Mooney et modélisé par un couplage entre une loi de Norton Hoff (glissement) et le modèle de Cross (cisaillement). La sensibilité au traitement thermomécanique est prise en compte par un facteur de glissement énergétique fonction de l'énergie spécifique et de la température matière. La troisième partie valide les modèles et leur implémentation dans un logiciel de simulation de remplissage REM3D. L'injection du PU est réalisée dans un moule transparent. Basés sur la visualisation, le titrage et le suivi de température, les résultats sont en accord avec la simulation au niveau cinétique. Pour le caoutchouc, un moule spirale est utilisé. Dans le moule, les pressions mesurées et calculées sont proches. Un écart apparaît dans la buse et est attribué aux effets élongationnels non pris en compte dans le modèle visqueux utilisé.

Les phases de validation et de vérification (V&V) des systèmes réactifs temps réel critique (de plus en plus complexes) sont très importantes en termes de coût et de temps. Dans ce contexte, toute méthode et outil permettant d'aider à la réalisation des activités de V&V est d'une très grande importance au cours du développement. Le test fonctionnel est le moyen le plus utilisé au cours de ces phases de V&V. Or, les méthodes de test présentent des limites : un test exhaustif est quasiment impossible à réaliser en raison de la taille et de la complexité des systèmes considérés. Dans ce contexte, les enjeux de la maîtrise de l'effort de test (complexité et coût) sont majeurs, mais les exigences de qualité pour ces systèmes sont très grandes. L'effort de test caractérise tout autant l'élaboration des jeux de test que le diagnostic. Dans cette optique, nous avons défini deux méthodologies basées sur les concepts d'analyse de testabilité et les stratégies de test. La première méthodologie permet d'aider à la définition de jeux de test pertinents et à l'analyse de couverture des systèmes réactifs spécifiés dans un formalisme flot de données SCADE dans le contexte AIRBUS. La seconde propose des méthodes d'aide à la vérification (identification de tests pertinents et localisation de composants défectueux au cours diagnostic) de systèmes sur la chaîne d'assemblage finale (FAL) d'un avion AIRBUS.