Le thème principal de cette recherche est d'étudier et développer des techniques pour la modélisation des systèmes où la sécurité est critique. Cette thèse est focalisé sur l'étape de la spécification du domaine où de tels systèmes vont fonctionner, et de sa validation. La contribution de cette thèse est double. D'abord, nous modélisons le domaine des transports terrestres, un bon candidat pour cette étude en raison de sa nature critique vis-à-vis de la sécurité, dans le cadre formel de B événementiel et proposent quelques directives pour cette activité. Ensuite, nous présentons une approche, basée sur les techniques de l'animation et des transformations, pour la validation par étapes des spécifications formelles.

Le festival n'est pas une activité a-juridique. Cette activité événementielle attractive est encadrée par les pouvoirs publics tant par des mesures de police administrative que dans son occupation du domaine public. Cet événement présentant incontestablement des atouts pour la politique touristique et culturelle d'un territoire est devenu une véritable institution cofinancée par les pouvoirs publics. Oscillant entre mission de service public et simple activité de prestation de services, la question de l'intérêt public local de cette activité est au cœur d'un contentieux émergent devant le juge administratif. Dans le même temps, la valeur du festival tend à se privatiser. L'introduction du mécénat, le recours à certains droits de propriété intellectuelle pour protéger cette valeur (droit des marques pour l'appellation et le droit d'auteur pour la programmation) et le travail des groupes de pression pour obtenir un nouveau droit voisin en faveur des organisateurs de spectacles sont autant d'indices qui illustrent ce mouvement de privatisation. De plus, la tentation d'appropriation des concepts festivaliers incite à proposer une qualification juridique globale pour laquelle la notion de fonds de commerce s'avère adaptée. Enfin, l'application de contrats de franchise ou de partenariat aux festivals constitue des instruments juridiques utiles pour permettre leurs duplications.

Les événements urbains festifs (EUF) s'imposent non seulement comme de nouvelles pratiques sociales, mais aussi en tant qu'action urbaine et objet d'analyse de la recherche urbaine. Ils agissent sur l'espace public suivant des logiques distinctes éphémères, cycliques, immatérielles des actions urbaines " traditionnelles " et des modalités actuelles de gestion de tels espaces. Aussi, cette recherche vise à appréhender si les logiques de gestion des EUF ouvrent de nouvelles perspectives pour la gestion des espaces publics. Pour répondre à ce questionnement, le cadre théorique de la " Gestion de site " a été mobilisé. Ce dernier décrit et permet d'appréhender les modalités de gestion de quatre sites urbains (gares multimodales, centres-villes, centres commerciaux, résidences privées avec services) complexes (du point de vue de la coexistence de fonctions, de services urbains, d'usages et d'intérêts sectoriels, spécifiques), permanents, de natures distinctes et proposant des ambiances particulières à leurs usagers.Il est apparu que ce cadre théorique permettait bien d'appréhender les modalités de gestion d'autres sites urbains aussi complexes que ceux analysés par la " Gestion de site ", et pourtant de nature éphémères : les sites de déroulement des EUF. Ce cadre théorique a donc été confronté à deux EUF se déroulant sur des sites éphémères : " Bordeaux-fête-le-vin " et les " Rendez-vous de l'Erdre " à Nantes. Ce choix est motivé principalement par le fait que ces EUF sont mis en place précisément sur des sites composés par une série d'espaces publics dont la gestion quotidienne et événementielle est complexe : les " espaces publics fluviaux ". L'analyse de la gestion de ces deux EUF par le prisme de la " Gestion de site " met en évidence des enseignements sur la gestion de l'événementiel qui, d'une part, nourrissent la réflexion autour de la gestion des espaces publics complexes et, d'autre part, enrichissent la " Gestion de site " en apportant des éléments inédits à ce cadre théorique nouveau

Cette thèse porte sur la spécification, la vérification et la validation de systèmes critiques à l'aide de méthodes formelles, en particulier, B événementiel. Nous avons travaillé sur l'utilisation de B événementiel pour étudier des algorithmes de contrôle du platooning, à partir d'une version 1D simplifiée vers une version 2D plus réaliste. L'analyse critique du modèle du platooning en 1D a découvert certaines anomalies. La difficulté d'exprimer les théorèmes de deadlock-freeness dans B événementiel nous a motivé pour développer un outil, le générateur de théorèmes de deadlock-freeness, pour construire automatiquement ces théorèmes. Notre évaluation a confirmé que les preuves mathématiques ne sont pas suffisantes pour vérifier la correction d'une spécification formelle : une spécification formelle doit aussi être validée. Nous pensons que les activités de validation, comme les activités de vérification, doivent être associées à chaque raffinement. Pour ce faire, nous avons besoin de meilleurs outils de validation. Certains outils d'exécution existants échouent pour certains modèles non-déterministes exprimés en B événementiel. Nous avons donc conçu et implanté un nouvel outil d'exécution, JeB, un environnement de simulation en JavaScript pour B événementiel. JeB permet aux utilisateurs d'insérer du code sûr à la main pour fournir des calculs déterministes lorsque la traduction automatique échoue. Pour atteindre cet objectif, nous avons défini des obligations de preuve qui garantissent la correction de simulations par rapport au modèle formel / This thesis aims at the specification, verification and validation of safety-critical systems with formal methods, in particular, with Event-B. We assessed the usability of Event-B by the development of platooning control algorithms, specially how it scaled up from a simplified 1D version to a more realistic 2D version. The critical analysis of the 1D platooning model uncovered some anomalous behaviors. The difficulty of expressing the deadlock-freeness theorems in Event-B motivated us to develop a tool, the generator of deadlock-freeness theorems, to automatically construct these theorems. Our assessment confirmed that the mathematical proofs are not sufficient to assure the correctness of a formal specification: a formal specification should also be validated. We believe that the validation activities, like the verification activities, should be associated with each refinement during the development. To do that, we need better validation tools. The state-of-the-art tools which can execute Event-B models failed in highly non-deterministic models. Therefore we designed and implemented a new execution tool, JeB, which is a JavaScript simulation framework for Event-B. JeB allows users to safely insert hand-coded pieces of code to supply deterministic computations where the automatic translation fails. To achieve this goal, we have defined a set of proof-obligations which, when discharged, guarantee the correctness of the simulations with respect to the model.

Le festival n'est pas une activité a-juridique. Cette activité événementielle attractive est encadrée par les pouvoirs publics tant par des mesures de police administrative que dans son occupation du domaine public. Cet événement présentant incontestablement des atouts pour la politique touristique et culturelle d'un territoire est devenu une véritable institution cofinancée par les pouvoirs publics. Oscillant entre mission de service public et simple activité de prestation de services, la question de l'intérêt public local de cette activité est au cœur d'un contentieux émergent devant le juge administratif. Dans le même temps, la valeur du festival tend à se privatiser. L'introduction du mécénat, le recours à certains droits de propriété intellectuelle pour protéger cette valeur (droit des marques pour l'appellation et le droit d'auteur pour la programmation) et le travail des groupes de pression pour obtenir un nouveau droit voisin en faveur des organisateurs de spectacles sont autant d'indices qui illustrent ce mouvement de privatisation. De plus, la tentation d'appropriation des concepts festivaliers incite à proposer une qualification juridique globale pour laquelle la notion de fonds de commerce s'avère adaptée. Enfin, l'application de contrats de franchise ou de partenariat aux festivals constitue des instruments juridiques utiles pour permettre leurs duplications. / A festival is a legal activity. This attractive entertaining event is regulated by the government as well through administrative policies measures as by its occupation of the public domain. This event, undoubtedly providing with potential assets for tourism and cultural policies of a given territory, has become an institution cofinanced by public authorities. Oscillating between public service mission and plain private service provision, the issue of local public interest of this activity is at the heart of an emerging dispute before the administrative law judge. At the same time, the value of the festival tends to become privatized. The introduction of corporate philanthropy and sponsoring, the use of specific intellectual property rights to protect that value (name branding laws for the designation and copyright laws for the programming) and groups lobbying for new laws to protect event organizers are all indicators that illustrate the privatization trend. Moreover, the temptation of appropriation of festival concepts fosters the proposal of a comprehensive legal qualification for which the concept of business is appropriate. Finally, the application of franchise or partnership to the festivals provides legal instruments useful to enable their duplication.

Le travail de thèse présente une méthode de développement de systèmes automatisés basée sur les méthodes formelles B et TLA+. Le développement par raffinement est au cœur de la méthode proposée. Un système automatisé est modélisé par deux composants, un contrôlé formé par le dispositif physique et son environnement et un contrôleur pilotant ce dernier. Il est exprimé par un produit synchronisé sur les actions de ces deux composants. La première contribution de la thèse concerne la proposition d'une approche qui combine le B événementiel et le langage de modélisation TLA+ pour la vérification des propriétés de vivacité. Nous définissons une extension syntaxique et sémantique du B événementiel permettant d'exprimer des propriétés de vivacité. Nous développons un prototype pour la transformation d'un modèle B en un module TLA+ sur lequel nous effectuons la preuve des propriétés de vivacité avec le model checker TLC. Pour la vérification de ce type de propriétés sur des systèmes infinis, nous proposons l'utilisation des diagrammes de prédicats qui sont des abstractions des systèmes modélisés en TLA+. La deuxième contribution est la proposition d'une technique pour représenter explicitement le temps en B événementiel. Cette technique s'appuie sur la réalisation d'un entrelacement entre un processus qui gère le temps avec les autres processus du système. Le temps modélisé est discret et son écoulement est modélisé par des événements. Cette approche est assez différente des systèmes temporisés où l'on considère que le temps s'écoule indépendamment du système. Dans la troisième contribution, nous proposons une approche de développement des systèmes automatisés en utilisant la technique de composition où il s'agit de développer conjointement le contrôleur et le composant physique qu'il contrôle et appliquer le raffinement aussi bien sur le contrôleur que le contrôlé. Le raffinement est une technique de base des méthodes que nous proposons et si notre objectif est de construire des contrôleurs corrects, le critère de correction porte sur le comportement du système automatisé qui résulte de la composition du contrôleur et du contrôlé. Nous présentons également un théorème de compositionnalité qui indique sous quelles conditions il est possible de déduire que le composé des raffinements des contrôleur et contrôlé est un raffinement du composé des contrôleur et contrôlé abstraits. La dernière contribution porte sur la définition, la preuve et l'utilisation d'un patron de raffinement pour les processus continus dans des systèmes de production manufacturière. Ce type de patron prouvé permet d'utiliser l'abstraction discrète de l'effet d'un processus continu agissant pendant un certain temps / This thesis deals with the development of automated systems while following the formal methods B and TLA+. We propose a formal methodology based on the refinement paradigm to specify and verify the system that we model by two components: the controlled system representing the physical device and its environment, and the controller that controls the system. A synchronised product on the actions of these two components is applied to specify the automated system. As a first contribution, we propose an approach combining the event B method and the language TLA+ in order to verify liveness properties defined in user requirements. Inspired by the temporal logic of actions TLA, we first extend the event B notation to specify liveness properties and we give semantics of this extended syntax over traces. Second, we give transformation rules from a temporal B model into a TLA+ module. We present, in particular, our prototype system called B2TLA+, that we have developed to support this transformation. To consider infinite systems, we use predicate diagrams as abstractions of systems modelled with TLA+. To consider the real-time concept in automated systems, we propose as a second contribution a technique explicitly representing time in B event systems. This technique is based on an interleaving between any event handling time and the other system events. By considering the well known co-design technique, we propose as a third contribution a refinement-based composition technique keeping a separation between controller and controlled systems in order to build correct automated systems satisfying user requirements. We prove a compositionality theorem with respect to refinement to get an efficient approach to verify the refinement of a synchronized composition between components. We verify the refinement of a synchronized composition by verifying separately the refinement of each component. Finally, we define, prove and use in a case study as a fourth contribution the concept of a refinement pattern for continuous processes in manufacturing systems. Such proven pattern allows us to use the discrete abstraction of the effect of continuous processes operating for a while

Face aux défis actuels liés à la conception de capteurs d'images à forte résolution comme la limitation de la consommation électrique, l'augmentation du flux de données ainsi que le traitement de données associé, on propose, à travers cette thèse, un capteur d'image novateur asynchrone à échantillonnage non uniforme.Ce capteur d’images asynchrone est basé sur une matrice de pixels événementiels qui intègrent un échantillonnage non uniforme par traversée de niveaux. Contrairement aux imageurs conventionnels, où les pixels sont lus systématiquement lors de chaque trame, les pixels événementiels proposés sont consultés que lorsqu’ils contiennent une information pertinente. Cela induit un flux de données réduit et dépendant de l’image.Pour compléter la chaîne de traitement des pixels, on présente également une architecture numérique de lecture dédiée conçue en utilisant de la logique asynchrone et destinée à contrôler et à gérer le flux de données des pixels événementiels. Ce circuit de lecture numérique permet de surmonter les difficultés classiques rencontrées lors de la gestion des demandes simultanées des pixels événementiels sans dégrader la résolution et le facteur de remplissage du capteur d’images. En outre, le circuit de lecture proposé permet de réduire considérablement les redondances spatiales dans une image ce qui diminue encore le flux de données.Enfin, en combinant l'aspect échantillonnage par traversée de niveau et la technique de lecture proposée, on a pu remplacer la conversion analogique numérique classique de la chaîne de traitement des pixels par une conversion temps-numérique (Time-to-Digital Conversion). En d'autres termes, l'information du pixel est codée par le temps. Il en résulte une diminution accrue de la consommation électrique du système de vision, le convertisseur analogique-numérique étant un des composants les plus consommant du système de lecture des capteurs d'images conventionnels / In order to overcome the challenges associated with the design of high resolution image sensors, we propose, through this thesis, an innovative asynchronous event-driven image sensor based on non-uniform sampling. The proposed image sensor aims the reduction of the data flow and its associated data processing by limiting the activity of our image sensor to the new captured information.The proposed asynchronous image sensor is based on an event-driven pixels that incorporate a non-uniform sampling crossing levels. Unlike conventional imagers, where the pixels are read systematically at each frame, the proposed event-driven pixels are only read when they hold new and relevant information. This induces a reduced and scene dependent data flow.In this thesis, we introduce a complete pixel reading sequence. Beside the event-driven pixel, the proposed reading system is designed using asynchronous logic and adapted to control and manage the flow of data from event pixels. This digital reading system overcomes the traditional difficulties encountered in the management of simultaneous requests for event pixels without degrading the resolution and fill factor of the image sensor. In addition, the proposed reading circuit significantly reduces the spatial redundancy in an image which further reduces the data flow.Finally, by combining the aspect of level crossing sampling and the proposed reading technique, we replaced the conventional analog to digital conversion of the pixel processing chain by a time-to-digital Conversion (TDC). In other words, the pixel information is coded by time. This results in an increased reduction in power consumption of the vision system, the analog-digital converter being one of the most consuming reading system of conventional image sensors components

Les événements urbains festifs (EUF) s'imposent non seulement comme de nouvelles pratiques sociales, mais aussi en tant qu'action urbaine et objet d'analyse de la recherche urbaine. Ils agissent sur l'espace public suivant des logiques distinctes éphémères, cycliques, immatérielles des actions urbaines « traditionnelles » et des modalités actuelles de gestion de tels espaces. Aussi, cette recherche vise à appréhender si les logiques de gestion des EUF ouvrent de nouvelles perspectives pour la gestion des espaces publics. Pour répondre à ce questionnement, le cadre théorique de la « Gestion de site » a été mobilisé. Ce dernier décrit et permet d'appréhender les modalités de gestion de quatre sites urbains (gares multimodales, centres-villes, centres commerciaux, résidences privées avec services) complexes (du point de vue de la coexistence de fonctions, de services urbains, d'usages et d'intérêts sectoriels, spécifiques), permanents, de natures distinctes et proposant des ambiances particulières à leurs usagers.Il est apparu que ce cadre théorique permettait bien d'appréhender les modalités de gestion d'autres sites urbains aussi complexes que ceux analysés par la « Gestion de site », et pourtant de nature éphémères : les sites de déroulement des EUF. Ce cadre théorique a donc été confronté à deux EUF se déroulant sur des sites éphémères : « Bordeaux-fête-le-vin » et les « Rendez-vous de l'Erdre » à Nantes. Ce choix est motivé principalement par le fait que ces EUF sont mis en place précisément sur des sites composés par une série d'espaces publics dont la gestion quotidienne et événementielle est complexe : les « espaces publics fluviaux ». L'analyse de la gestion de ces deux EUF par le prisme de la « Gestion de site » met en évidence des enseignements sur la gestion de l'événementiel qui, d'une part, nourrissent la réflexion autour de la gestion des espaces publics complexes et, d'autre part, enrichissent la « Gestion de site » en apportant des éléments inédits à ce cadre théorique nouveau / Festive urban events (EUF) stand out not only as new social practices, but also as urban actions providing a basis for urban research. Compared to "traditional" urban actions and current methods of public space management, Festive urban events in public spaces follow different dynamics ; they are ephemeral, cyclic, and immaterial. This research examines the management implications of Festive urban events and attempts to determine if these events' dynamics can unlock new perspectives for public space management.To answer our research enquiries, a Management of site (GS) theoretical framework is used. This theoretical framework describes and addresses the common management methods of four urban sites : multimodal rail stations, downtown areas, shopping malls, and private residences with services. These four site types are complexes, incorporating the coexistence of multiple urban functions and services, varied practices and interacting sector-based interests. These site types are permanent and offer a unique ambiance to their users. It appeared early on that a Management of site framework also allows describing the management methods of another kind of urban site, ephemeral nature, which seems as complex as those previously analyzed by this theoretical framework: the ephemeral sites in which Festive urban events are held. The Management of site framework was therefore examined with two different Festive urban events taking place in an ephemeral site : Bordeaux-fête-le-vin in the city of Bordeaux and the Rendez-vous de l'Erdre in the city of Nantes. This choice was made largely because these Festive urban events are held in ephemeral sites comprised of a number of different yet interacting components that require complex management : riverbank public places. The analysis of management methods of both these Festive urban events through the prism of the Management of site framework provides substantial insight into special event management. This insight enhances our understanding of complex public space manag ement and enriches the Management of site framework by introducing new analysis criteria

Les crues « éclair » parfois dévastatrices qui touchent les bassins versants méditerranéens du Sud de la France sont difficiles à anticiper. Leur prévision passe par l'utilisation de modèles pluie-débit, dont l'efficacité est encore limitée par les incertitudes liées notamment à la variabilité spatiale des pluies méditerranéennes et à la caractérisation de l'état hydrique initial des hydrosystèmes. Dans le cas de bassins karstiques, à ces incertitudes s'ajoutent celles liées à la dynamique des aquifères et à leur rôle sur la formation des crues. La première partie de ce travail de thèse propose un modèle pluie-débit horaire, distribué, événementiel et parcimonieux pour reproduire les crues « éclair » à l'exutoire du bassin karstique du Lez (Montpellier) de 114 km2. Le modèle est évalué non seulement sur la qualité des simulations de débits mais aussi sur la qualité de son initialisation obtenu grâce à une relation entre sa condition initiale et divers indicateurs de l'état hydrique de l'hydrosystème. Calibré sur 21 épisodes de crues, le modèle fournit des simulations satisfaisantes, et sa condition initiale est significativement corrélée à l'indice d'humidité Hu2 du modèle SIM de Météo-France ou à la piézométrie dans l'aquifère du Lez. Les pluies mesurées par radar en début d'automne sont de bonne qualité et conduisent à une amélioration des simulations de débit et de l'estimation de la condition initiale du modèle. En revanche, les pluies mesurées par radar en fin d'automne sont de moindre qualité et n'améliorent pas les simulations. Face aux incertitudes liées à la paramétrisation du modèle ou à l'estimation des pluies radar, la deuxième partie du travail de thèse analyse l'apport de l'assimilation des débits observés pour corriger en temps réel les paramètres les plus sensibles du modèle et notamment sa condition initiale ou les pluies radar en entrée du modèle. La procédure d'assimilation de données a été mise en place à l'aide du coupleur PALM, qui permet de relier modèle hydrologique à l'algorithme d'assimilation. La correction de la condition initiale du modèle permet généralement d'améliorer les prévisions (sous hypothèse de pluie future connue); la correction de la pluie a des effets similaires. Néanmoins les limites de cette correction sont atteintes dans le cas où le modèle ne reproduit pas de façon satisfaisante la partie initiale de montée des eaux, ce qui pourra être amélioré par la suite. Finalement, ce travail de thèse montre que la complexité d'un bassin karstique peut être représentée efficacement à l'aide d'un nombre réduit de paramètres, pour simuler les débits, et contribue à l'amélioration des outils opérationnels pour la prévision des crues. / The sometimes devastating flash floods which affect the Mediterranean watersheds of the South of France are difficult to anticipate. Flood forecasting requires the use of rainfall-runoff models which are limited in their efficiency by uncertainty related to the spatial variability of Mediterranean rainfall and the characterization of the initial hydric state of the system. In karstic catchments, these uncertainties are added to those due to aquifer dynamics and their role in flood genesis. The first part of this work will present a distributed event-based parsimonious hourly rainfall-runoff model in order to reconstruct flash flood events at the outlet of the 114 km2 Lez Catchment (Montpellier). The model is evaluated not only for the quality of the simulations produced, but for the quality of its parameter initialization obtained using a relationship between the initial condition and various hydric state indicators of the system. Calibrated using 21 flood episodes, the model produces satisfactory simulations and its initial condition is significantly correlated with the Hu2 soil humidity index of the Météo-France model or piezometers measuring the Lez aquifer. Radar rainfall data measured in early fall are of good quality and lead to improved discharge simulations and an improved estimation of the model initial condition. However, rainfall measured by radar in late fall are of poor quality and do not improve the simulations. Confronted with the uncertainty related to model parametrization or the estimation of radar rainfall, the second part of this dissertation analyzes improvements achieved by assimilating observed discharge measurements in order to perform real-time corrections to the most sensitive model parameters and notably the initial condition and the radar rainfall input to the model. The data assimilation procedure was implemented with the help of the PALM coupling software which allows for the linking of the hydrological model with the assimilation algorithm. Correcting the initial condition allowed for, on average, the improvement of forecasting (under a known future rainfall hypothesis); correcting the rainfall had similar effects. Nevertheless, the limits of this approach are reached when the model is unable to satisfactorily reproduce the rising limb of the hydrograph, a problem which may be addressed by future research. Finally, this body of work demonstrates that the complexity of a karstic catchment can be efficiently represented with a reduced number of parameters in order to simulate discharges and contribute to the improvement of operational tools for flood forecasting.

Les événements urbains festifs (EUF) s'imposent non seulement comme de nouvelles pratiques sociales, mais aussi en tant qu'action urbaine et objet d'analyse. Ils agissent sur l'espace public suivant des logiques distinctes – éphémères, cycliques, immatérielles – des actions urbaines « traditionnelles » et des modalités actuelles de gestion de tels espaces. Aussi, cette recherche vise à appréhender si les logiques de gestion des EUF ouvrent de nouvelles perspectives pour la gestion des espaces publics. Pour répondre à ce questionnement, le cadre théorique de la « Gestion de site » a été mobilisé. Ce dernier décrit les modalités de gestion de quatre sites urbains (gares multimodales, centres-villes, centres commerciaux, résidences privées avec services) complexes (du point de vue de la coexistence de fonctions, de services urbains, d'usages et d'intérêts sectoriels, spécifiques), permanents, de natures distinctes et proposant des ambiances particulières. Il est apparu que ce cadre théorique permettait bien d'appréhender les modalités de gestion d'autres sites urbains aussi complexes que ceux analysés par la « Gestion de site », et pourtant de nature éphémères : les sites de déroulement des EUF. Ce cadre théorique a donc été confronté à deux EUF se déroulant sur des sites éphémères : « Bordeaux-fête-le-vin » et les « Rendez-vous de l'Erdre » à Nantes. Ce choix est motivé principalement par le fait que ces EUF sont mis en place précisément sur des sites composés par une série d'espaces publics dont la gestion – quotidienne et événementielle – est complexe : les « espaces publics fluviaux ». L'analyse de la gestion de ces deux EUF par le prisme de la « Gestion de site » met en évidence des enseignements sur la gestion de l'événementiel qui, d‟une part, nourrissent la réflexion autour de la gestion des espaces publics complexes et, d'autre part, enrichissent la « Gestion de site » en apportant des éléments inédits à ce cadre théorique nouveau.