Dans cette thèse, nous abordons le problème de la modélisation et de la vérification de systèmes complexes présentant des comportements à la fois probabilistes et temporisés. La conception de tels systèmes est devenue de plus en plus complexe en raison de l’hétérogénéité des composants impliqués, l’incertitude découlant d’un environnement ouvert et les contraintes temps réelinhérentes à leurs domaines d’application. La gestion à la fois du logiciel et du matériel dans une vue unifiée tout en incluant des informations sur les performances (par exemple, temps de calcul et de communication, consommation d’énergie, etc.) devient indispensable. Construire et analyser des modèles de performance est d’une importance primordiale pour donner des garanties sur les exigences fonctionnelles et extra-fonctionnelles des systèmes, et permettre uneprise de décision fondée sur des mesures quantitatives dès les premières étapes de la conception.Cette thèse apporte plusieurs nouvelles contributions. Tout d’abord, nous introduisons un nouveau formalisme de modélisation appelé BIP stochastique et temps réel (SRT-BIP) pour la modélisation, la simulation et la génération de code de systèmes à base de composants. Ce formalisme hérite du framework BIP ses capacités de modélisation basées sur les composants et le temps réel et, en outre, il fournit des primitives pour exprimer des comportements stochastiquescomplexes.Deuxièmement, nous étudions des techniques d’apprentissage automatique pour faciliter la construction de modèles de performance. Nous proposons d’améliorer et d’adapter une procédure d’apprentissage présentée dans la littérature pour déduire des modèles stochastiques et temporisés à partir d’exécutions concrètes du système, et de les exprimer dans le formalisme SRT-BIP.Troisièmement, étant donné les modèles de performance dans SRT-BIP, nous explorons l’utilisation du model checking statistique (SMC) pour l’analyse d’exigences concernant la fonctionnalité et les performances du système. Pour ce faire, nous fournissons un framework complet, appelé SBIP, en tant qu’outil de support pour la modélisation, la simulation et l’analyse des systèmes SRT-BIP. SBIP est un environnement de développement intégré (IDE) qui implémente des algorithmes SMC pour des analyses quantitatives, qualitatives et d’événementsrares, en plus d’une procédure d’automatisation pour l’exploration des paramètres d’une propriété. Nous validons nos propositions sur des études de cas réels touchant à des domaines variés tels que les protocoles de communication, les systèmes concurrents et les systèmesembarqués.Enfin, nous étudions plus en détail l’intérêt du SMC lorsqu’il est inclus dans des méthodes d’analyse de système élaborées. Nous illustrons cela en proposant deux approches d’évaluation des risques. Dans la première approche, nous introduisons une méthodologie en spirale pour modéliser des systèmes résilients avec des composants FDIR que nous validons à travers l’évaluation de la sécurité du système de locomotion d’un rover d’exploration planétaire. La deuxième approche concerne l’évaluation des politiques de sécurité des organisations selon une approche de sécurité offensive. L’objectif est de synthétiser des configurations de défense efficaces contre des stratégies d’attaque optimisées (qui minimisent le coût d’attaque et maximisent la probabilité de succès). Ces stratégies d’attaque sont obtenues en combinant l’apprentissage de modèles et les méthodes méta-heuristiques, dans lesquels le SMC a le rôle principal d’évaluer et de prioriser les potentielles stratégies candidates. / In this thesis, we address the problem of modeling and verification of complex systems exhibiting both probabilistic and timed behaviors. Designing such systems has become increasingly complex due to the heterogeneity of the involved components, the uncertainty resulting from open environment and the real-time constraints inherent to their application domains. Handling both software and (abstraction of) hardware in a unified view while also including performanceinformation (e.g. computation and communication times, energy consumption, etc.) becomes a must. Building and analyzing performance models is of paramount importance in order to give guarantees on the functional and extra-functional system requirements and to make well-founded design decisions based on quantitative measures at early design stages.This thesis brings several new contributions. First, we introduce a new modeling formalism called Stochastic Real-Time BIP (SRT-BIP) for the modeling, the simulation and the code generation of component-based systems. This formalism inherits from the BIP framework its component-based and real-time modeling capabilities and, extends it by providing comprehensive primitives to express complex stochastic behaviors.Second, we investigate machine learning techniques to ease the construction of performance models. We propose to enhance and adapt a state-of-the-art learning procedure to infer stochastic real-time models from concrete system execution and to represent them in the SRT-BIP formalism.Third, given performance models in SRT-BIP, we explore the use of statistical Model Checking (SMC) for the anaysis of system’s functional and performance requirements. To do so, we provide a full framework, called SBIP, as a support tool for the modeling, simulation and analysis of SRT-BIP systems. SBIP is an Integrated Development Environment (IDE) that implements SMC algorithms for quantitative, qualitative and rare events analyses together with an automated exploring procedure for parameterized requirements. We validate our proposalson real-life case studies ranging from communication protocols and concurrent systems to embedded systems.Finally, we further investigate the interest of SMC when included in elaborated system analysis workflows. We illustrate this by proposing two risk assessment approaches. In the first approach, we introduce a spiral methodology to build resilient systems with FDIR components that we validate on the safety assessment of a planetary rover locomotion system. The second approach is concerned with the security assessment of organization’s defenses following an offensive security approach. The goal is to synthesize impactful defense configurations against optimized attack strategies (that minimize attack cost and maximize success probability). These attack strategies are obtained by combining model learning with meta heuristics, and where SMC is used to score and prioritize potential candidate strategies.

Les réseaux de capteurs sans fil ont connu depuis quelques années un intérêt majeur dans tous les domaines d’activités. Une des informations attendue est la localisation des nœuds capteurs ; pourtant, compte-tenu des contraintes imposées aux capteurs en termes d’encombrement et d’énergie, il est peu envisageable d’équiper le capteur d’équipements spécifiques dédié à la localisation comme un récepteur GPS. Dès lors, localiser le capteur en exploitant le signal de communication est une option intéressante. A l’inverse des techniques Range-Free exploitant des hypothèses de connectivité du réseau, les techniques généralement connues pour atteindre une bonne précision de localisation par la radio sont de type Range-Based, et se basent, dans notre cas, sur la mesure du temps de vol du signal radio UWB. Nos contributions portent alors sur le choix d’une couche physique performante, sur la mise en place d’outils favorisant une bonne précision temporelle dans les échanges radio, et l’élaboration d’un protocole original d’évaluation de la distance. Les travaux présentés dans ce manuscrit visent donc à aborder la problématique générale de la localisation d’intérieur dans les réseaux de capteurs sans fil, et en particulier la fonctionnalité de ranging qui est le mécanisme d’évaluation de la distance entre les nœuds. Dans un premier temps, nous implémentons puis évaluons les protocoles de référence rencontrés dans la littérature. Nous identifions et corrigeons par la suite, les erreurs susceptibles de biaiser la métrique du temps de vol. Nous proposons alors le protocole 2M-TWR (2 Messages – Two Way Ranging) comme une amélioration du protocole de référence TWR. Enfin, nous proposons et implémentons le protocole BB-TWR (Beacon Based –TWR), qui permet d’effectuer le ranging, de manière séquentielle et non séquentielle, en incluant les informations temporelles nécessaires dans tout trafic natif diffusé existant. Les preuves de concept ont été prototypées et évaluées sur un banc de test réel. / In recent years, Wireless Sensor Networks has gained an important interest in all fields of activity. One of the expected information is the sensor nodes localization; However, due to the sensors constraints in terms of memory and energy, it is not possible to equip the sensor with specific equipment dedicated to the localization as the GPS receiver. Thus, locating the sensor by using the communication signal is an interesting option. In contrast to Range-Free techniques which use assumptions of network connectivity, the Range-Based techniques are known to reach good localization accuracy and, in our case, they are based on the measurement of the time of flight of the radio signal UWB. Our contributions focus on the choice of an efficient physical layer, on the implementation of tools that promote a good temporal accuracy in radio exchanges, and the development of an original distance evaluation protocol. Research works presented in this manuscript aim to address the global general problem of indoor localization in wireless sensor networks, and particularly the ranging functionality which is the distance evaluation mechanism between nodes. At first we implemented and evaluated the well-known protocols encountered in the literature. Then, we identify and correct errors that may bias the Time of flight metric. We propose the 2M-TWR protocol (2 Messages - Two Way Ranging) as an improvement to the TWR reference protocol. Finally, we propose and implement the BB-TWR (Beacon Based-TWR) protocol, which is able to perform ranging, sequentially and non-sequentially, by including the necessary time information in any existing broadcast native traffic. The proofs of concept were prototyped and evaluated on a real testbed.

L'objectif de ce travail de thèse dans un premier temps est l'évaluation de performances des modèles de routage multi-chemins pour l'ingénierie de trafic et l'équilibrage de charge sur un réseau de type IP/MPLS (MPLS-TE). Nous comparons la capacité de ces modèles à équilibrer la charge du réseau tout en faisant de la différentiation de trafic. Nous les appliquons sur des grandes topologies générées par le générateur automatique des topologies BRITE, qui s'approchent en forme et en complexité du réseau réel. Nous mesurons ainsi l'impact de leur complexité respective et donc la capacité à les déployer sur des réseaux de grande taille (scalabilité). Dans un second temps, l'objectif est de proposer un concept de modélisation générale d'un réseau à commutations par paquets. Ce modèle est établi sur la base de la théorie différentielle de trafic et la théorie des files d'attente, tout en utilisant des approches graphiques. Le but est d'estimer l'état de charge du réseau et de ses composants (routeurs, liens, chemins). Ensuite, en fonction de ça, nous développons des approches de contrôle de congestion et commande sur l'entrée améliorant les techniques de routage adaptatif et l'équilibrage de charge dans les réseaux IP/MPLS / In This work, firstly we present and evaluate the behavior of multipath routing models for the DS-TE (DiffSev aware MPLS traffic Engineering) called PEMS and LBWDP. To clarify network topologies and routing models that are suitable for MPLS Traffic Engineering, we evaluate them from the viewpoint of network scalability and end-to-end quality. Using a network topology generated by BRITE, that has many alternative paths, we applied these models on a huge topology that correspond to real network. This can provide a real simulation for the internet and gives a good evaluation for the end-to-end quality and the network use.Secondly, the aim of this work is to propose a general model for Packet switching networks. This model is established on the traffic differential theory and the Queuing theory, while using graphic approaches. The aim of this model is to calculate the network use state and its components (router, link, path...). Then, we develop control and command approaches in the entry of network to improve an adaptive routing plan and load balancing in IP/MPLS networks

Cette thèse traite de la modélisation et la simulation de réseaux de capteurs sans fil afin de fournir des estimations précises de consommations d´énergie. Un cadre de conception et de simulation base sur SystemC au niveau système est proposé, nommé IDEA1. Elle permet l’exploration de l’espace de conception de réseaux de capteurs à un stade amont. Les résultats de simulation comprennent le taux de livraison de paquets, la latence de transmission et les consommations d’énergie. Sur un banc d’essai comportant 9 nœuds, la différence moyen entre les IDEA1 simulations et les mesures expérimentales est 4.6 %. Les performances d'IDEA1 sont comparées avec un autre simulateur largement utilisé, NS-2. Avec la co-simulation matérielle et logicielle, IDEA1 peut apporter des modèles plus détaillés de nœuds de capteurs. Pour fournir les résultats de la simulation au même niveau d’abstraction, IDEA1 réalise les simulations deux fois plus vite que NS-2.Enfin, deux études de cas sont accomplies pour valider le flot de conception d'IDEA1. La performance de l‘IEEE 802.15.4 est globalement évaluée pour diverses charges de trafic et configurations de paramètres de protocole. Une application de contrôle actif des vibrations est également étudiée. Les simulations d'IDEA1 trouvent le meilleur choix de protocoles de communication. / This thesis deals with the modeling and simulation of wireless sensor networks in order to provide mote accurate prediction of energy consumptions. A SystemC-based system level design and simulation framework is proposed, named as IDEA1. It enables the design space exploration of sensor networks at an early stage. The simulation results include packet delivery rate, transmission latency and energy consumptions. A testbed consisting of 9 motes is built to validate the simulation results of IDEA1. The average deviation between the IDEA1 simulations and the experimental measurements is 4.6%. The performances of IDEA1 are compared with a widely-used WSN simulator,NS-2. With the hardware and software co-simulation, IDEA1 can provide more detailed models of sensor nodes. For offering the simulation results at same abstraction level,IDEA1 only uses one third of the simulation time of NS-2. Finally, two case studies are performed to validate design flow of IDEA1. The performance of IEEE 802.15.4sensor networks is comprehensively evaluated for various traffic loads and configurations of protocol parameters. In addition, a real-time active vibration control application is also studied. By the simulation of IDEA1, the best choice of communication protocols and hardware platforms is found.