Les systèmes temps réel et distribués posent des problèmes complexes en termes de conception d'architecture et de description de comportements. De par leur criticité en vies humaines et leurs coûts de prototypage, ces systèmes ont motivé le développement d'une activité de recherche sur les langages de modélisation formelle et les techniques de validation basées modèle qui contribuent à la détection au plus tôt des erreurs de conception. Néanmoins, les langages formels ont eu un succès plus que limité dans l'industrie. L'arrivée du langage UML (Unified Modeling Language) a ouvert de nouveaux horizons pour l'intégration de langages de modélisation formelle dans une méthodologie de conception susceptible d'être mieux acceptée par les praticiens du domaine. En s'appuyant sur une expérience antérieure de la technique de description formelle Estelle et des extensions temporelles des réseaux de Petri, notre activité de recherche sur les cinq dernières années a débouché sur la production d'un profil UML nommé TURTLE (Timed UML and RT-LOTOS Environment). TURTLE surpasse UML 2.0 par ses extensions aux diagrammes d'analyse et de conception UML, sa sémantique formelle exprimée en RT-LOTOS, et ses outils de support (éditeur de diagrammes et outil de validation formelle combinant simulation et vérification basée sur une analyse daccessibilité). La méthodologie TURTLE trouve son champ d'application naturel dans la conception de systèmes temps réel et la validation d'architectures de communication en particulier. L'approche proposée a été appliquée avec succès à des systèmes satellitaires et des protocoles d'authentification.

La mobilité est une composante importante de la liberté des personnes. L'évolution des moyens technologiques y contribue au premier chef. Outre la question du transport, celle du maintien du lien entre les individus est en ce sens particulièrement prégnante. Elle a mis à rude épreuve la notion de réseaux de télécommunications puisqu'il s'agit de répondre, pour des individus éparpillés ou concentrés, mais mobiles, au besoin de rester reliés. De l'ère des réseaux analogiques à celle des réseaux numériques, de l'ère des réseaux filaires à celle des réseaux sans fil et mobiles, la technologie n'a cessé d'évoluer. Ces dernières décennies ont vu apparaître des réseaux numériques sans fil, où non seulement il y a mobilité des utilisateurs mais aussi mobilité de l'infrastructure du réseau à laquelle ils contribuent. Ces réseaux se constituent de façon spontanée. Ils se maintiennent de manière autonome. On les désigne par le terme réseaux ad hoc mobiles (en anglais Mobile Ad hoc Networks ou MANET) qui s'oppose naturellement à celui de réseaux à infrastructure. La sécurité est une préoccupation générale des êtres humains. Ils en ressentent aussi le besoin en matière de réseaux. Ce besoin est particulièrement criant lorsque sont échangées des données critiques, financières ou stratégiques. La confidentialité des échanges, l'authentification des sources, l'assurance d'intégrité, la prévention de la récusation sont autant d'objectifs qu'il faut alors atteindre. Diverses solutions de sécurité ont été conçues dans cette optique pour les réseaux filaires puis ont ensuite été adaptées aux réseaux sans-fil et mobiles. Les architectures AAA (Authentication, Authorization, Accounting) en font partie. Elles sont en général utilisées dans un contexte commercial. Tant par leur facilité de déploiement que par la baisse des coûts de mise en œuvre qu'ils engendrent, les réseaux ad hoc mobiles, après avoir bien servi dans le domaine militaire, semblent avoir un avenir dans les applications commerciales. C'est pourquoi, nous nous proposons dans cette thèse de concevoir une architecture AAA adaptée aux spécificités de ces réseaux. Nous étudions d'abord les réseaux ad hoc mobiles et leurs caractéristiques. Ensuite, nous présentons les solutions de sécurité qui existent dans les réseaux à infrastructure. Nous examinons, en particulier, les solutions qui permettent le contrôle d'accès et dont sont engendrées les architectures AAA. Les solutions AAA proposées pour les MANETs sont par la suite analysées et classifiées afin de déterminer les manques et les vulnérabilités. Cette étude approfondie nous amène à proposer une architecture AAA répondant aux attentes identifiées. C'est une architecture distribuée qui répond, en particulier, au besoin d'autonomie des opérations dans les MANETs et où les protocoles exécutés peuvent impliquer simultanément plus de deux parties. Un ensemble de protocoles et de mécanismes d'authentification et d'autorisation s'intégrant avec la suite des protocoles IPv6 a été proposé. Leur sécurité a été discutée. Celle, en particulier du protocole d'authentification a fait l'objet de validation formelle. Contrairement aux protocoles utilisés dans la phase d'autorisation des services AAA proposés, le mode de communication multi-parties et multi-sauts du protocole d'authentification nous a poussé à mener une analyse approfondie de ses performances. Pour cela, nous avons eu recours, dans un premier temps, à la modélisation au moyen de calculs mathématiques explicites ensuite à la simulation. Les résultats obtenus montrent que ce protocole passe à l'échelle d'un MANET comprenant au moins cent nœuds. Dans certaines conditions d'implémentation que nous avons définies, ses performances, tant celle liée à sa probabilité de terminaison avec une issue favorable que celle portant sur son temps d'exécution, atteignent des valeurs optimales.

Modélisation globale de l'énergie dans les réseaux de capteurs (incluant le matériel, les couches protocolaires, l'application, et l'environnement physique).<br />Application de méthodes de validation formelle au cas des réseaux de capteurs. <br />Etude de cas du projet ANR ARESA.

Il y a un besoin grandissant pour d'autonomie dans des systèmes temps réel complexes tels que les robots ou les satellites. Ceci met en avant un problème non trivial : d'un côté il y a des systèmes complexes - donc difficiles à valider - avec une intervention de l'humain dans la boucle qui se veut minimale, de l'autre nous avons des domaines où il faut que le système ait un comportement sûr fonctionnellement afin d'éviter les coûts financiers et/ou humains d'une perte ou d'une détérioration du système. Ces deux notions mises en vis-à-vis semblent contradictoires. En effet comment être sûr qu'un système autonome avec un pouvoir décisionnel fort, n'aura pas un comportement non nominal qui pourra menacer le bon déroulement de la mission ? Comment être sûr qu'un satellite n'allumera pas ses réacteurs sans avoir protégé ses capteurs fragiles (objectif de la caméra, ...) ? Une réponse partielle à ce type de problèmes pourrait être d'utiliser un planificateur de haut niveau qui ne donnerait que des plans garantis comme sûrs et valides. Toutefois ces planificateurs n'ont pas un modèle complet des actions qu'ils effectuent et de leurs conséquences. En effet, les directives données par ce planificateur sont généralement affinées en sous tâches par un superviseur. Le planificateur n'a donc pas un contrôle complet sur le moyen d'effectuer cette action. Nous présentons ici les travaux effectués afin d'intégrer un système de contrôle d'exécution en ligne dans une architecture hiérarchisée. Nous décrivons ici la nécessité et le rôle d'un tel composant dans ce type d'architecture. Nous introduisons le R2C, notre contrôleur basé sur les hypothèses synchrones, ainsi que l'outil permettant sa génération en exploitant des techniques issues du model-checking symbolique. Enfin nous discutons de la nécessité de prendre en compte les com-posants décisionnels dans le contrôle afin d'interférer le moins possible avec les décisions prises par ceux-ci. Les résultats obtenus durant des expérimentations sur une plate-forme robotique confirment les idées développées au cours de ce travail et permettent d'en tirer les conclusions et perspectives sur la mise en place d'un contrôle pour l'amélioration de la fiabilité globale de tels systèmes.

La méthodologie HILECOP a été élaborée pour la conception formelle de systèmes numériques complexes critiques ; elle couvre donc l'intégralité du processus, allant de la modélisation à la génération de code pour l’implantation sur la cible matérielle (composant électronique de type FPGA), en passant par la validation formelle. Or, si le modèle formel, les réseaux de Petri en l'occurrence, est par essence asynchrone, il est néanmoins exécuté de manière synchrone sur la cible. De fait, les approches d'analyse usuelles ne sont pas adaptées au sens où elles construisent des graphes d'états non conformes à l'évolution d'états réelle au sein de la cible. Dans l'objectif de gagner en confiance quant à la validité des résultats de l’analyse formelle, ces travaux visent à capturer les caractéristiques dites non-fonctionnelles, à les réifier sur le modèle et enfin à considérer leur impact à travers l’analyse. En d’autres termes, l’objectif est d’améliorer l’expressivité du modèle et la pertinence de l'analyse, en considérant des aspects comme la synchronisation d'horloge, le parallélisme effectif, le risque de blocage induit par l'expression conjointe d'un événement (condition) et d'une fenêtre temporelle d'occurrence, sans omettre la gestion des exceptions. Pour traiter tous ces aspects, nous avons proposé une nouvelle méthode d'analyse pour les réseaux de Petri temporels généralisés étendus interprétés exécutés en synchrone, en les transformant vers un formalisme équivalent analysable. Ce formalisme est associé avec une sémantique formelle intégrant toutes les aspects particuliers de l'exécution et un algorithme de construction d'un graphe d'états spécifique : le Graphe de Comportement Synchrone. Nos travaux ont été appliqués à un cas industriel, plus précisément à la validation du comportement de la partie numérique d'un neuro-stimulateur. / The HILECOP methodology has been developed for the formal design of critical complex digital systems; it therefore covers the entire design process, ranging from modeling to code generation for implementation on the hardware target (FPGA type electronic component), via formal validation. However, if the formal model, the Petri nets in this case, is inherently asynchronous, it is nevertheless executed synchronously on the target. In fact, the usual analysis approaches are not adapted in the sense that they construct state graphs that do not conform to the real state evolution within the target. In order to gain confidence in the validity of the results of the formal analysis, this work aims to capture the so-called non-functional characteristics, to reify them on the model and finally to consider their impact through the analysis.In other words, the aim is to improve the expressiveness of the model and the relevance of the analysis, considering aspects such as clock synchronization, effective parallelism, the risk of blocking induced by the expression of an event (condition) and a time window of occurrence, without omitting the management of exceptions.To deal with all these aspects, we have proposed a new method of analysis for extended generalized synchronous executed time Petri nets, transforming them into an analysable equivalent formalism. This formalism is associated with a formal semantics integrating all the particular aspects of the execution and dédicated state space construction algorithm: the Synchronous Behavior Graph.Our work has been applied to an industrial case, more precisely to the validation of the behavior of the digital part of a neuro-stimulator.

La mobilité est une composante importante de la liberté des personnes. L’évolution des moyens technologiques y contribue au premier chef. Outre la question du transport, celle du maintien du lien entre les individus est en ce sens particulièrement prégnante. Elle a mis à rude épreuve la notion de réseaux de télécommunications puisqu’il s’agit de répondre, pour des individus éparpillés ou concentrés, mais mobiles, au besoin de rester reliés. De l’ère des réseaux analogiques à celle des réseaux numériques, de l’ère des réseaux filaires à celle des réseaux sans fil et mobiles, la technologie n’a cessé d’évoluer. Ces dernières décennies ont vu apparaître des réseaux numériques sans fil, où non seulement il y a mobilité des utilisateurs mais aussi mobilité de l’infrastructure du réseau à laquelle ils contribuent. Ces réseaux se constituent de façon spontanée. Ils se maintiennent de manière autonome. On les désigne par le terme réseaux ad hoc mobiles (en anglais Mobile Ad hoc Networks ou MANET) qui s’oppose naturellement à celui de réseaux à infrastructure. La sécurité est une préoccupation générale des êtres humains. Ils en ressentent aussi le besoin en matière de réseaux. Ce besoin est particulièrement criant lorsque sont échangées des données critiques, financières ou stratégiques. La confidentialité des échanges, l’authentification des sources, l’assurance d’intégrité, la prévention de la récusation sont autant d’objectifs qu’il faut alors atteindre. Diverses solutions de sécurité ont été conçues dans cette optique pour les réseaux filaires puis ont ensuite été adaptées aux réseaux sans-fil et mobiles. Les architectures AAA (Authentication, Authorization, Accounting) en font partie. Elles sont en général utilisées dans un contexte commercial. Tant par leur facilité de déploiement que par la baisse des coûts de mise en œuvre qu’ils engendrent, les réseaux ad hoc mobiles, après avoir bien servi dans le domaine militaire, semblent avoir un avenir dans les applications commerciales. C’est pourquoi, nous nous proposons dans cette thèse de concevoir une architecture AAA adaptée aux spécificités de ces réseaux. Nous étudions d’abord les réseaux ad hoc mobiles et leurs caractéristiques. Ensuite, nous présentons les solutions de sécurité qui existent dans les réseaux à infrastructure. Nous examinons, en particulier, les solutions qui permettent le contrôle d’accès et dont sont engendrées les architectures AAA. Les solutions AAA proposées pour les MANETs sont par la suite analysées et classifiées afin de déterminer les manques et les vulnérabilités. Cette étude approfondie nous amène à proposer une architecture AAA répondant aux attentes identifiées. C’est une architecture distribuée qui répond, en particulier, au besoin d’autonomie des opérations dans les MANETs et où les protocoles exécutés peuvent impliquer simultanément plus de deux parties. Un ensemble de protocoles et de mécanismes d’authentification et d’autorisation s’intégrant avec la suite des protocoles IPv6 a été proposé. Leur sécurité a été discutée. Celle, en particulier du protocole d’authentification a fait l’objet de validation formelle. Contrairement aux protocoles utilisés dans la phase d’autorisation des services AAA proposés, le mode de communication multi-parties et multi-sauts du protocole d’authentification nous a poussé à mener une analyse approfondie de ses performances. Pour cela, nous avons eu recours, dans un premier temps, à la modélisation au moyen de calculs mathématiques explicites ensuite à la simulation. Les résultats obtenus montrent que ce protocole passe à l’échelle d’un MANET comprenant au moins cent nœuds. Dans certaines conditions d’implémentation que nous avons définies, ses performances, tant celle liée à sa probabilité de terminaison avec une issue favorable que celle portant sur son temps d’exécution, atteignent des valeurs optimales. / Mobility is an important component of people’s liberty. The evolution of technological means contributes to its enhancement. In addition to the transport issue, the question of keeping people connected is, in that context, particularly significant. Technological change strained the notion of telecommunications networks in the sense that scattered or clustered but mobile individuals had to remain in touch with others electronically. From the age of analogue networks to the digital networks era, from wired networks to wireless and mobile networks, technology has never stopped evolving. The last decades have witnessed the emergence of digital and wireless networks where not only the users, but also the network infrastructure to which they contribute, are mobile. These networks are spontaneously formed and autonomously maintained. They are termed Mobile Ad hoc Networks (MANETs), in contradistinction to infrastructure networks. Security is a general concern of human beings. They feel the need for it when using a network, too. This need is particularly glaring when it comes to exchanging critical, financial or strategic data. Confidentiality of communications, source authentication, integrity assurance, prevention of repudiation, are all objectives to be achieved. Various security solutions have been devised in this context as wired networks were then adapted to wireless and mobile networks. AAA (Authentication, Authorization and Accounting) frameworks are among these solutions. They are generally used for commercial purposes, which raises financial issues — and we all know how much important they are. Due to their ease of deployment and inexpensive implementation, MANETs, first used in the military field, seem to have a future in commercial applications. That is why the present thesis proposes to design an AAA service that is adapted to the characteristics of such networks. In this perspective, the thesis examines, to begin with, mobile ad hoc networks in order to understand their characteristics and potentials. It then probes the security solutions that exist in infrastructure networks, with special emphasis on those dealing with access control and AAA services. The AAA solutions for MANETs proposed up to now are subsequently analyzed and classified in order to determine their strengths and weaknesses. This in-depth study led to the design, in the second part of the thesis, of an AAA service that meets the expectations identified. It is a distributed service intended to answer the needs of autonomous operations in MANETs when a nearby operator is absent. It features several detailed authentication and authorization mechanisms and protocols with an authentication protocol simultaneously involving one or more parties. These protocols are designed such that they can be easily integrated to the IPv6 protocols suite. Moreover, their security is discussed — in particular, that of the authentication protocol thanks to a formal validation tool. Unlike the communication mode of the authorization protocols, that of the authentication protocol is one-to-many, which led us to study more deeply its performances thanks to modeling using explicit mathematical computations and to simulations techniques. The obtained results showed that the protocol scales for a MANET including a hundred nodes. Under certain conditions that we explained, its performances, in terms of the probability of authentication success and the length of the executing time, reach optimal values.

La conception de systèmes embarqués modernes est de plus en plus complexe, car plus de fonctionnalités sont intégrées dans ces systèmes. En même temps, afin de répondre aux exigences de calcul tout en conservant une consommation d'énergie de faible niveau, MPSoCs sont apparus comme les principales solutions pour tels systèmes embarqués. En outre, les systèmes embarqués sont de plus en plus adaptatifs, comme l’adaptabilité peut apporter un certain nombre d'avantages, tels que la flexibilité du logiciel et l'efficacité énergétique. Cette thèse vise la conception sécuritaire de ces MPSoCs adaptatifs. Tout d'abord, chaque configuration de système doit être analysée en ce qui concerne ses propriétés fonctionnelles et non fonctionnelles. Nous présentons un cadre abstraite de conception et d’analyse qui permet des décisions d’implémentation plus rapide et plus rentable. Ce cadre est conçu comme un support de raisonnement intermédiaire pour les environnements de co-conception de logiciel / matériel au niveau de système. Il peut élaguer l'espace de conception à sa plus grande portée, et identifier les candidats de solutions de conception de manière rapide et efficace. Dans ce cadre, nous utilisons un codage basé sur l’horloge abstrait pour modéliser les comportements du système. Différents scénarios d'applications de mapping et de planification sur MPSoCs sont analysés via les traces d'horloge qui représentent les simulations du système. Les propriétés d'intérêt sont l’exactitude du comportement fonctionnel, la performance temporelle et la consommation d'énergie. Deuxièmement, la gestion de la reconfiguration de MPSoCs adaptatifs doit être abordée. Nous sommes particulièrement intéressés par les MPSoCs implémentés sur des architectures reconfigurables de hardware (ex. FPGA tissus) qui offrent une bonne flexibilité et une efficacité de calcul pour les MPSoCs adaptatifs. Nous proposons un cadre général de conception basésur la technique de la synthèse de contrôleurs discrets (SCD) pour résoudre ce problème. L’avantage principal de cette technique est qu'elle permet une synthèse d'un contrôleur automatique vis-à-vis d’une spécification donnée des objectifs de contrôle. Dans ce cadre, le comportement de reconfiguration du système est modélisé en termes d'automates synchrones en parallèle. Le problème de calcul de la gestion reconfiguration vis-à-vis de multiples objectifs concernant, par exemple, les usages des ressources, la performance et la consommation d’énergie est codé comme un problème de SCD . Le langage de programmation BZR existant et l’outil Sigali sont employés pour effectuer SCD et générer un contrôleur qui satisfait aux exigences du système. Finalement, nous étudions deux façons différentes de combiner les deux cadres de conception proposées pour MPSoCs adaptatifs. Tout d'abord, ils sont combinés pour construire un flot de conception complet pour MPSoCs adaptatifs. Deuxièmement, ils sont combinés pour présenter la façon dont le gestionnaire d'exécution conçu dans le second cadre peut être intégré dans le premier cadre de sorte que les simulations de haut niveau peuvent être effectuées pour évaluer le gestionnaire d'exécution. / The design of modern embedded systems is getting more and more complex, as more func- tionality is integrated into these systems. At the same time, in order to meet the compu- tational requirements while keeping a low level power consumption, MPSoCs have emerged as the main solutions for such embedded systems. Furthermore, embedded systems are be- coming more and more adaptive, as the adaptivity can bring a number of benefits, such as software flexibility and energy efficiency. This thesis targets the safe design of such adaptive MPSoCs. First, each system configuration must be analyzed concerning its functional and non- functional properties. We present an abstract design and analysis framework, which allows for faster and cost-effective implementation decisions. This framework is intended as an intermediate reasoning support for system level software/hardware co-design environments. It can prune the design space at its largest, and identify candidate design solutions in a fast and efficient way. In the framework, we use an abstract clock-based encoding to model system behaviors. Different mapping and scheduling scenarios of applications on MPSoCs are analyzed via clock traces representing system simulations. Among properties of interest are functional behavioral correctness, temporal performance and energy consumption. Second, the reconfiguration management of adaptive MPSoCs must be addressed. We are specially interested in MPSoCs implemented on reconfigurable hardware architectures (i.e., FPGA fabrics), which provide a good flexibility and computational efficiency for adap- tive MPSoCs. We propose a general design framework based on the discrete controller syn- thesis (DCS) technique to address this issue. The main advantage of this technique is that it allows the automatic controller synthesis w.r.t. a given specification of control objectives. In the framework, the system reconfiguration behavior is modeled in terms of synchronous parallel automata. The reconfiguration management computation problem w.r.t. multiple objectives regarding e.g., resource usages, performance and power consumption is encoded as a DCS problem. The existing BZR programming language and Sigali tool are employed to perform DCS and generate a controller that satisfies the system requirements. Finally, we investigate two different ways of combining the two proposed design frame- works for adaptive MPSoCs. Firstly, they are combined to construct a complete design flow for adaptive MPSoCs. Secondly, they are combined to present how the designed run-time manager by the second framework can be integrated into the first framework so that high level simulations can be performed to assess the run-time manager.

La sécurité est un enjeu majeur dans le cycle de développement des systèmes critiques, notamment dans le secteur du transport ferroviaire. Cette thèse vise la modélisation, la vérification et la validation des règles d'exploitation ferroviaires au regard des exigences de sécurité. Ces règles ont pour but de définir les autorisations de déplacement des trains sur des lignes ferroviaires nationales équipées du système européen de gestion du trafic ferroviaire (ERTMS). De manière analogue, on trouve les concepts liés aux autorisations dans la description des politiques de contrôle d'accès des systèmes d'information. Par conséquent, nos contributions portent sur l'adaptation d'une approche UML/B pour le contrôle d'accès des systèmes d'information afin de modéliser et de valider les règles d'exploitation ferroviaires. Dans un premier temps, nous avons adapté le modèle Role Based Access Control (RBAC) sur une étude de cas ferroviaire extraite des règles d'exploitation appliquées sur la ligne à grande vitesse LGV Est-Européenne en France. La plate-forme B4MSecure nous a permis de modéliser ces règles à l'aide d'un profil UML de RBAC inspiré de SecureUML. Ensuite, ces modèles sont transformés en des spécifications B qui ont été enrichies par des propriétés de sécurité ferroviaire et soumises à des activités de vérification et de validation formelles. Aux concepts du modèle RBAC, le modèle Organization Based Access Control (Or-Bac) introduit la notion d'organisation, au centre de ce modèle, et la notion de contexte. Nous avons donc proposé d’utiliser ce modèle en tant qu’extension du modèle RBAC dans l’optique d’une interopérabilité ferroviaire en ERTMS. / The safety is a major issue in the development cycle of the critical systems, in particular in the rail transportation sector. This thesis aims at the modeling, the verification and at the validation of the railway operating rules with regard to the safety requirements. These rules intend to define the authorizations of trains movement on national railway lines equipped with the European Rail Traffic Management System (ERTMS). In a similar way, we find the concepts of authorizations in the description of access control policies of information systems. Consequently, our contributions concern the adaptation of an UML/B approach for the access control of information systems to model and validate the railway operating rules. At first, we adapted the Role Based Access Control (RBAC) model on a railway case study extracted from the operating rules applied on the LGV-Est-Européenne line in France. The B4MSecure platform enables the modeling of these rules by means of a UML profile of RBAC inspired by SecureUML. Then, these models are transformed into B specifications. which are enhanced by railway safety properties and formally verified and validated. In addition to the concepts of the RBAC model, the Organization Based Access Control (Or-Bac) model introduces the notion of organization, in the center of this model, and the notion of context. We have therefore proposed to use this model as extension of the RBAC model in the context of railway interoperability in ERTMS.

Nous développons une méthode de modélisation et de validation adaptée aux système parallèles structurés en couches hiérarchiques. Nous définissons deux notions : la concordance de modèle prouve que le modèle possède bien les propriétés dégagées par les spécifications; l'adéquation de service valide le protocole par rapport à son service. Nous appliquons notre méthode à la modélisation du protocole de télécommunication de niveau Transport (la couche 4 d'après la norme ISO sur l'interconnexion des systèmes ouverts). Nous étudions tout particulièrement la gestion de désynchronisations du Service de la couche Réseau, et le contrôle de flux avec réquisition de crédit du protocole de la couche Transport. Nous utilisons les réseaux de Petri à prédicats pour décrire le modèle du service rendu par le couche Réseau sous-jacente et nous en servir pour construire le modèle du protocole de ma couche Transport. nous prouvons que la notion d'abstraction peut s'étendre aux réseaux de Petri à prédicats. La preuve du déroulement correct du protocole est apportée en utilisant les invariants issus du modèle.