Search

The design of communication protocols is generally based on functional models developed from the system needs. In Intelligent Transport Systems (ITS), the studied functionalities include self-organization, routing, reliability, quality of service and security. Simulation evaluations of ITS protocols mainly focus on performance in specific scenarios. However, the evolution of transportation towards autonomous vehicles requires robust protocols offering guarantees on some of their properties. Formal approaches make it possible to provide automatic proof of certain properties, but for others it is necessary to use interactive proof involving the knowledge of an Expert. The work carried out in this thesis aims to develop, in the DEVS formalism (Discrete Event System Specification), models of an ITS whose simulation would make it possible to observe the properties, possibly verified by a formal approach, in a broader scenario and to generate data on the models that could feed an interactive proof loop instead of an Expert. Targeting the CBL-OLSR (Chain-Branch-Leaf in Optimized Link State Routing) protocol, this thesis shows how a DEVS model and an equivalent formal Event-B model can be built from the same functional specification of an ad hoc network where nodes use this protocol. Safety and security properties are introduced into the formal Event-B model to be verified, and a methodology is proposed to transfer them to an equivalent DEVS model in the form of constraints, choices or observables according to preproposed criteria. Finally, this thesis also opens up the prospects for automating this design process, integrating real data on both road traffic and vehicle application flows into DEVS simulation, and interacting with specialized simulators for the various components (e. g. MATLAB for propagation models, OPNET or NS3 for communications, SUMO for mobility models); the aim being to evaluate the protocol in a very realistic system context., La conception de protocoles de communication repose généralement sur des modèles fonctionnels élaborés à partir des besoins du système.Dans les systèmes de transport intelligents (ITS), les fonctionnalités étudiées incluent l’auto-organisation, le routage, la fiabilité, la qualité de service et la sécurité. Les évaluations par simulation sur les protocoles dédiés aux ITS se focalisent sur les performances dans des scénarios spécifiques. Or, l’évolution des transports vers les véhicules autonomes nécessite des protocoles robustes offrant des garanties sur certaines de leurs propriétés. Les approches formelles permettent de fournir la preuve automatique de certaines propriétés, mais pour d’autres il est nécessaire de recourir à une preuve interactive impliquant le savoir d’un Expert. Les travaux menés dans cette thèse poursuivent l’objectif d’élaborer, dans le formalisme DEVS (Discrete Event System Specification), des modèles d’un ITS dont la simulation permettrait d’observer les propriétés, éventuellement vérifiées par une approche formelle, dans un scénario plus large et de générer sur les modèles des données susceptibles d’alimenter une boucle de preuve interactive au lieu d’un Expert. Prenant pour cible le protocole CBL-OLSR (Chain-Branch- Leaf inOptimized Link State Routing), cette thèse montre comment un modèle DEVS et un modèle formel Event-B équivalents peuvent être construits à partir de la même spécification fonctionnelle d’un réseau ad hoc où les nœuds utilisent ce protocole. Des propriétés relatives à la sûreté et à la sécurité sont introduites dans le modèle formel Event-B afin d’être vérifiées, puis une méthodologie est proposée afin de les transférer dans un modèle DEVS équivalent sous forme de contraintes, de choix ou d’observables selon des critères proposés. Enfin, cette thèse ouvre également les perspectives de l’automatisation de ce processus de conception, de l’intégration à la simulation DEVS de données réelles à la fois sur le trafic routier et sur les flux d’applications dédiées aux véhicules, et de l’interaction avec des simulateurs spécialisés pour les différents composants (par exemple MATLAB pour les modèles de propagation, OPNET ou NS3 pour les communications, SUMO pour les modèles de mobilité) ; le but étant une évaluation du protocole dans un contexte très réaliste du système.

In the next years, electric vehicles (EVs) will make their appearance on the market. This even will have significant impact on the operation of the existing electricity networks which have to be updated to reach the new massive electricity demand. Moreover, EVs can also be seen as a new opportunity in the future electricity market. Indeed, a smart EV discharge / charge process can be enable a large power, valuable, and permanent storage media. The project's objectives are to: (1) propose a scheme integrating V2G interaction techniques: (a) adapt the grid functionality to the temporal and spatial constraints to the EV charging process in a residential setting. We seek to satisfy different power demands of EVs connected to the mains without stressing too smart grid, (b) optimizing the loading / unloading between EVs and the grid in both directions. (2) To propose new patterns of wireless communication between EVs and smart grid away from the charging stations, which are based on the standards of vehicle communications (VANET), as well as other communication standards on a large scale. Access to smart grid technologies will be introduced to negotiate the cost of charge / discharge, the waiting time of service, locations and also to plan consumer motivation to promote the grid stability, L’apparition massive des véhicules électriques (VEs) sur les marchés peut avoir un impact important sur le fonctionnement des réseaux d’électricité actuels qui devront ajuster leur fonctionnement à la nouvelle demande massive d'électricité provenant des VEs. Par contre, les VEs peuvent aussi être vus comme une nouvelle opportunité dans le futur marché d’électricité. En effet, une décharge/recharge intelligente peut permettre aux VEs d’être un support de stockage d’électricité important, valable et permanent dont la capacité croit en fonction du nombre des VEs. Ce projet a comme objectifs de : (1) proposer un schéma d’interaction V2G intégrant des techniques permettant de : (a) adapter le fonctionnement de la grille aux contraintes temporelles et spatiales relatives au processus de recharge des VEs dans un milieu résidentiel. (b) optimiser les opérations de chargement/déchargement entre les VEs et la grille dans les deux sens. (2) Proposer de nouveaux schémas de communication sans fil, entre les VEs et la grille intelligente loin des bornes de recharge, qui soient basés sur les standards de communications véhiculaires (VANET) ainsi que sur d’autres standards de communication à grande échelle. On introduira des techniques d’accès à la grille intelligente pour négocier le coût de recharge/décharge des batteries et aussi pour planifier la motivation du consommateur afin de favoriser la stabilité de la grille