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.

Le contexte de cette thèse est à l’intersection des contextes des grilles de calculs, des nouvelles technologies du Web ainsi que des Clouds et des services à la demande. Depuis leur avènement au cours des années 90, les plates-formes distribuées, plus précisément les systèmes de grilles de calcul (Grid Computing), n’ont pas cessé d’évoluer permettant ainsi de susciter multiple efforts de recherche. Les grilles de PCs ont été proposées comme une alternative aux super-calculateurs par la fédération des milliers d’ordinateurs de bureau. Les détails de la mise en oeuvre d’une telle architecture de grille, en termes de mécanismes de mutualisation des ressources, restent très difficile à cerner. Parallèlement, le Web a complètement modifié notre façon d’accéder à l’information. Le Web est maintenant une composante essentielle de notre quotidien. Les équipements ont, à leur tour, évolué d’ordinateurs de bureau ou ordinateurs portables aux tablettes, lecteurs multimédias, consoles de jeux, smartphones, ou NetPCs. Cette évolution exige d’adapter et de repenser les applications/intergiciels de grille de PCs qui ont été développés ces dernières années. Notre contribution se résume dans la réalisation d’un intergiciel de grille de PCs que nous avons appelé RedisDG. Dans son fonctionnement, RedisDG reste similaire à la plupart des intergiciels de grilles de calcul, c’est-à-dire qu’il est capable d’exécuter des applications sous forme de «sacs de tâches» dans un environnement distribué, assurer le monitoring des noeuds, valider et certifier les résultats. L’innovation de RedisDG, réside dans l’intégration de la modélisation et la vérification formelles dans sa phase de conception, ce qui est non conventionnel mais très pertinent dans notre domaine. Notre approche consiste à repenser les grilles de PCs à partir d’une réflexion et d’un cadre formel permettant de les développer, de manière rigoureuse et de mieux maîtriser les évolutions technologiques à venir. / The context of this work is at the intersection of grid computing, the new Web technologies and the Clouds and services on demand contexts. Desktop Grid have been proposed as an alternative to supercomputers by the federation of thousands of desktops. The details of the implementation of such an architecture, in terms of resource sharing mechanisms, remain very hard. Meanwhile, the Web has completely changed the way we access information. The equipment, in turn, have evolved from desktops or laptops to tablets, smartphones or NetPCs. Our approach is to rethink Desktop Grids from a reflexion and a formal framework to develop them rigorously and better control future technological developments. We have reconsidered the interactions between the traditional components of a Desktop Grid based on the Web technology, and given birth to RedisDG, a new Desktop Grid middelware capable to operate on small devices, ie smartphones, tablets like the more traditional devicves (PCs). Our system is entirely based on the publish-subscribe paradigm. RedisDG is developped with Python and uses Redis as advanced key-value cache and store.

Les neurones biologiques communiquent par le biais d’impulsions électriques, appelées spikes, et les fonctions cérébrales émergent notamment de la coordination entre les réceptions et émissions de ces spikes. Par ailleurs, il est largement admis que la fonction de chaque neurone dépend de sa morphologie. Les dendrites conditionnent l’intégration spatio-temporelle des spikes reçus et influent sur les temps d’occurrence des spikes émis. Elles sont donc fondamentales pour l’étude in silico des mécanismes de coordination, et en particulier pour l’étude des assemblées de neurones. Les modèles de neurones existants prenant en compte les dendrites, sont généralement des modèles mathématiques détaillés, souvent à base d’équations différentielles, dont la simulation nécessite des ressources de calculs importantes. De plus, leur complexité intrinsèque rend difficile l’analyse et les preuves sur ces modèles. Dans cette thèse, nous proposons un modèle de neurone intégrant des dendrites d’une manière abstraite. Dans l’objectif d’ouvrir la porte aux méthodes formelles, nous établissons une définition rigoureuse du cadre de modélisation et mettons en évidence des propriétés algébriques remarquables de l’intégration dendritique. Nous avons notamment démontré qu’il est possible de réduire la structure d’un neurone en préservant sa fonction d’entrée/sortie. Nous avons ainsi révélé des classes d’équivalence dont nous savons déterminer un représentant canonique. En s’appuyant sur la théorie des catégories et par des morphismes de neurones judicieusement définis, nous avons ensuite analysé plus finement ces classes d’équivalence. Un résultat surprenant découle de ces propriétés : un simple ajout de délais dans les modèles informatiques de neurones permet de prendre en compte une intégration dendritique abstraite, sans représenter explicitement la structure arborescente des dendrites. À la racine de l’arborescence dendritique, la modélisation du soma contient inévitablement une équation différentielle lorsque l’on souhaite préserver l’essence du fonctionnement biologique. Ceci impose de combiner une vision analytique avec la vision algébrique. Néanmoins, grâce à une étape préalable de discrétisation temporelle, nous avons également implémenté un neurone complet en Lustre qui est un langage formel autorisant des preuves par model checking. Globalement, nous apportons dans cette thèse un premier pas encourageant vers une formalisation complète des neurones, avec des propriétés remarquables sur l’intégration dendritique. / Biological neurons communicate by means of electrical impulses, called spikes. Brain functions emerge notably from reception and emission coordination between those spikes. Furthermore, it is widely accepted that the function of each neuron depends on its morphology. In particular, dendrites perform the spatio-temporal integration of received spikes and affect the occurrence of emitted spikes. Dendrites are therefore fundamental for in silico studies of coordination mechanisms, and especially for the study of so-called neuron assemblies. Most of existing neuron models taking into account dendrites are detailed mathematical models, usually based on differential equations, whose simulations require significant computing resources. Moreover, their intrinsic complexity makes difficult the analysis and proofs on such models. In this thesis, we propose an abstract neuron model integrating dendrites. In order to pave the way to formal methods, we establish a rigorous definition of the modeling framework and highlight remarkable algebraic properties of dendritic integration. In particular, we have demonstrated that it is possible to reduce a neuron structure while preserving its input/output function. We have thus revealed equivalence classes with a canonical representative. Based on category theory and thanks to properly defined neuron morphisms, we then analyzed these equivalence classes in more details. A surprising result derives from these properties: simply adding delays in neuron computational models is sufficient to represent an abstract dendritic integration, without explicit tree structure representation of dendrites. At the root of the dendritic tree, soma modeling inevitably contains a differential equation in order to preserve the biological functioning essence. This requires combining an analytical vision with the algebraic vision. Nevertheless, thanks to a preliminary step of temporal discretization, we have also implemented a complete neuron in Lustre which is a formal language allowing proofs by model checking. All in all, we bring in this thesis an encouraging first step towards a complete neuron formalization, with remarkable properties on dendritic integration.

Ce travail de thèse porte sur l'élaboration de modèles de haut-niveau de systèmes pluridisciplinaires à base d'électronique. L'objectif est de réaliser des prototypes virtuels de ces systèmes et de vérifier formellement leur comportement dès les premières étapes du cycle de conception. Grâce à une approche descendante et au formalisme HiLeS, nous réalisons des représentations hiérarchiques qui associent des réseaux de Petri à un ensemble de blocs et de canaux interagissant mutuellement. Nous avons développé l'outil HiLeS Designer pour rendre utilisable le formalisme avec plusieurs améliorations opérationnelles telles que le couplage avec un outil d'analyse de réseaux de Petri (TINA) et la compatibilité avec VHDL-AMS. Nous proposons donc, une plate-forme de conception amont autour de l'outil HiLeS Designer avec des passerelles vers TINA et VHDL-AMS. L'utilisation de cette plate-forme nous a permis d'identifier plusieurs perspectives de développement, notamment vers la conduite de projet.

Dans les années 90, la commission européenne a sollicité la mise au point d'un système de contrôle commande et de signalisation ferroviaire commun à tous les réseaux des états membres : le système ERTMS " European Railway Traffic Management System ". Il s'agit d'un système réparti complexe dont le déploiement complet est long et coûteux. L'objectif global consiste à diminuer les coûts de validation et de certification liés à la mise en œuvre de ce nouveau système en Europe. La problématique scientifique réside dans la modélisation formelle de la spécification afin de permettre la génération automatique des scénarios de test. Les verrous scientifiques, traités dans cette thèse, sont liés d'une part à la transformation de modèle semi-formel en modèle formel en préservant les propriétés structurelles et fonctionnelles des constituants réactifs du système réparti, et d'autre part à la couverture des tests générés automatiquement. Les constituants sont sous la forme de boîte noire. L'objectif consiste à tester ces derniers à travers la spécification ERTMS. Nous avons développé une approche de modélisation basée sur le couplage de modèles semi-formels (UML) et de modèles formels (Réseaux de Petri). Ce couplage se fait à travers une technique de transformation de modèles. Nous avons développé ensuite une méthode de génération automatique de scénarios de test de conformité à partir des modèles en réseaux de Petri. Les scénarios de test ont été considérés comme une séquence de franchissement filtrée puis réduite du réseau de Petri interprété représentant la spécification. Ces scénarios ont été exécutés sur notre plateforme de simulation ERTMS

Dans les années 90, la commission européenne a sollicité la mise au point d'un système de contrôle commande et de signalisation ferroviaire commun à tous les réseaux des états membres : le système ERTMS " European Railway Traffic Management System ". Il s'agit d'un système réparti complexe dont le déploiement complet est long et coûteux. L'objectif global consiste à diminuer les coûts de validation et de certification liés à la mise en œuvre de ce nouveau système en Europe. La problématique scientifique réside dans la modélisation formelle de la spécification afin de permettre la génération automatique des scénarios de test. Les verrous scientifiques, traités dans cette thèse, sont liés d'une part à la transformation de modèle semi-formel en modèle formel en préservant les propriétés structurelles et fonctionnelles des constituants réactifs du système réparti, et d'autre part à la couverture des tests générés automatiquement. Les constituants sont sous la forme de boîte noire. L'objectif consiste à tester ces derniers à travers la spécification ERTMS. Nous avons développé une approche de modélisation basée sur le couplage de modèles semi-formels (UML) et de modèles formels (Réseaux de Petri). Ce couplage se fait à travers une technique de transformation de modèles. Nous avons développé ensuite une méthode de génération automatique de scénarios de test de conformité à partir des modèles en réseaux de Petri. Les scénarios de test ont été considérés comme une séquence de franchissement filtrée puis réduite du réseau de Petri interprété représentant la spécification. Ces scénarios ont été exécutés sur notre plateforme de simulation ERTMS

Cette thèse traite de la vérification formelle de systèmes critiques où la correction du système dépend du respect des contraintes temporelles. La première partie étudie la modélisation et la vérification formelle par model-checking de systèmes temps réel dans le contexte de l’industrie aéronautique et spatiale. La deuxième partie décrit notre méthode d’exploitation des symétries pour les réseaux de Petri temporels. Nous définissons un opérateur de composition symétrique pour la construction de réseaux. Puis nous proposons des solutions pour la construction d’espaces d’états quotients par la relation d’équivalence induite par les symétries. Notre méthode s’applique aux réseaux de Petri, temporels ou non. A notre connaissance il s’agit de la première méthode applicable aux réseaux de Petri temporels. Des résultats expérimentaux encourageants sont présentés. / This thesis deals with formal verification of critical systems where the system’s correction depends on compliance with time constraints. The first part studies the formal modeling and verification by model-checking of realtime systems in the context of the aerospace industry. The second part describes our method for symmetry reduction of Time Petri Net. We define a symmetric composition operator for building Net. Then we present our solution for construction of quotients of the state spaces by the equivalence relation induced by symmetries. Our method applies to Petri nets, temporal or not, but to our knowledge this is the first methodology for Time Petri Nets. Encouraging experimental results are presented.

Les systèmes de production de type flow-shop sont des systèmes déterministes qui peuvent être modélisés analytiquement de manière relativement aisée dans une structure algébrique de dioïde. Les opérations dont est muni un dioïde sont essentiellement basées sur des phénomènes de synchronisation et de délai, ce qui permet d'aboutir à un modèle linéaire. Cependant, les systèmes de production manufacturiers présentent de plus en plus d'éléments hétérogènes en interaction et font ainsi partie d'une classe plus générale de systèmes, les job-shops. Ces interactions se caractérisent parfois par des conflits ; dès lors, une modélisation analytique linéaire n'est plus possible. En considérant un système à conflits, non plus directement, mais via ses comportements extrémaux, il est possible d'en obtenir une modélisation approchée, qui est linéaire dans un dioïde d'intervalles. Moyennant l'utilisation de règles d'affectation des ressources partagées et de politiques de routage appropriées, nous définissons des modèles linéaires de ces sections. On propose un modèle approché, dans un dioïde d'intervalles, de ces systèmes complexes, afin de bénéficier des contributions théoriques des structures algébriques de dioïde. Par ailleurs, les réseaux de Petri forment un outil graphique privilégié pour la représentation des systèmes dynamiques à événements discrets que sont les systèmes de production. Nous proposons une définition de la sémantique d'une sous-classe bien particulière de ces réseaux : les graphes d'événements temporisés à incertitudes temporelles, qui permettent de retranscrire des relations exprimées dans un dioïde d'intervalles. En somme, notre contribution permet d'étudier certains job-shops, alors que les possibilités actuelles se limitaient à l'étude de flow-shops.

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

Dans les années 90, la commission européenne a sollicité la mise au point d’un système de contrôle commande et de signalisation ferroviaire commun à tous les réseaux des états membres : le système ERTMS « European Railway Traffic Management System ». Il s’agit d’un système réparti complexe dont le déploiement complet est long et coûteux. L’objectif global consiste à diminuer les coûts de validation et de certification liés à la mise en œuvre de ce nouveau système en Europe. La problématique scientifique réside dans la modélisation formelle de la spécification afin de permettre la génération automatique des scénarios de test. Les verrous scientifiques, traités dans cette thèse, sont liés d’une part à la transformation de modèle semi-formel en modèle formel en préservant les propriétés structurelles et fonctionnelles des constituants réactifs du système réparti, et d’autre part à la couverture des tests générés automatiquement. Les constituants sont sous la forme de boîte noire. L’objectif consiste à tester ces derniers à travers la spécification ERTMS. Nous avons développé une approche de modélisation basée sur le couplage de modèles semi-formels (UML) et de modèles formels (Réseaux de Petri). Ce couplage se fait à travers une technique de transformation de modèles. Nous avons développé ensuite une méthode de génération automatique de scénarios de test de conformité à partir des modèles en réseaux de Petri. Les scénarios de test ont été considérés comme une séquence de franchissement filtrée puis réduite du réseau de Petri interprété représentant la spécification. Ces scénarios ont été exécutés sur notre plateforme de simulation ERTMS / European Union set up a European rail traffic management system “ERTMS” to ensure, with high level of safety, train operation on different European networks. As the full deployment of this system is long and expensive, evolutions are necessary and raise other technological challenges. The goal is to determine how to use ERTMS specifications to produce test scenarios. This work presents methods, models and tools dedicated to the generation of test scenarios for the validation of ERTMS components based on functional requirements. The development of ERTMS system requires adequate methods for Modelling and evaluating its behavior. Evaluation and certification of the system can be done by generating test scenarios applying formal methods. The Unified Modelling Language (UML) is a widely accepted Modelling standard in industry. However, it is a semi-formal language and it does not allow verification of system behavior. In this case, formal models like Petri Net can be used. These methods are used in order to formalize ERTMS specification. Tests scenarios are generated on the basis of Petri net models. One scenario is considered like a firing sequence in the reachability graph of the Petri net. Then, test scenarios are applied on ERTMS platform simulator in order to check the components and to give test verdicts. Finally, the approach, developed in this document, has been applied to ERTMS components in order to demonstrate the validation and certification costs reduction and also to minimize the upgrade and retrofit constraints and validation cost