Internet applications have been extended to various aspects of everyday life and offer services of high reliability and security. In the Academia, Internet applications offer useful tools for the remote creation of simulation models and real-time conduction of control experiments. The aim of this study was the design of a reliable, safe and secure software system for real time operation of a remote aero gas turbine, with the use of standard Internet technology at very low cost. The gas turbine used in this application was an AMT Netherlands Olympus micro gas turbine. The project presented three prototypes: operation from an adjacent computer station, operation within the Local Area Netwok (LAN) of Cranfield University and finally, remotely through the Internet. The gas turbine is a safety critical component, thus the project was driven by risk assessment at all the stages of the software process, which adhered to the Spiral Model. Elements of safety critical systems design were applied, with risk assessment present in every round of the software process. For the implementation, various software tools were used, with the majority to be open source API’s. LabVIEW with compatible hardware from National Instruments was used to interface the gas turbine with an adjacent computer work station. The main interaction has been established between the computer and the ECU of the engine, with additional instrumentation installed, wherever required. The Internet user interface web page implements AJAX technology in order to facilitate asynchronous update of the individual fields that present the indications of the operating gas turbine. The parameters of the gas turbine were acquired with high accuracy, with most attention given to the most critical indications, exhaust gas temperature (EGT) and rotational speed (RPM). These are provided to a designed real-time monitoring application, which automatically triggers actions when necessary. The acceptance validation was accomplished with a formal validation method – Model Checking. The final web application was inspired by the RESTful architecture and allows the user to operate the remote gas turbine through a standard browser, without requiring any additional downloading or local data processing. The web application was designed with provisions for generic applications. It can be configured to function with multiple different gas turbines and also integrated with external performance simulation or diagnostics Internet platforms. Also, an analytical proposal is presented, to integrate this application with the TURBOMATCH WebEngine web application, for gas turbine performance simulation, developed by Cranfield University.

Internet applications have been extended to various aspects of everyday life and offer services of high reliability and security. In the Academia, Internet applications offer useful tools for the remote creation of simulation models and real-time conduction of control experiments. The aim of this study was the design of a reliable, safe and secure software system for real time operation of a remote aero gas turbine, with the use of standard Internet technology at very low cost. The gas turbine used in this application was an AMT Netherlands Olympus micro gas turbine. The project presented three prototypes: operation from an adjacent computer station, operation within the Local Area Netwok (LAN) of Cranfield University and finally, remotely through the Internet. The gas turbine is a safety critical component, thus the project was driven by risk assessment at all the stages of the software process, which adhered to the Spiral Model. Elements of safety critical systems design were applied, with risk assessment present in every round of the software process. For the implementation, various software tools were used, with the majority to be open source API’s. LabVIEW with compatible hardware from National Instruments was used to interface the gas turbine with an adjacent computer work station. The main interaction has been established between the computer and the ECU of the engine, with additional instrumentation installed, wherever required. The Internet user interface web page implements AJAX technology in order to facilitate asynchronous update of the individual fields that present the indications of the operating gas turbine. The parameters of the gas turbine were acquired with high accuracy, with most attention given to the most critical indications, exhaust gas temperature (EGT) and rotational speed (RPM). These are provided to a designed real-time monitoring application, which automatically triggers actions when necessary. The acceptance validation was accomplished with a formal validation method – Model Checking. The final web application was inspired by the RESTful architecture and allows the user to operate the remote gas turbine through a standard browser, without requiring any additional downloading or local data processing. The web application was designed with provisions for generic applications. It can be configured to function with multiple different gas turbines and also integrated with external performance simulation or diagnostics Internet platforms. Also, an analytical proposal is presented, to integrate this application with the TURBOMATCH WebEngine web application, for gas turbine performance simulation, developed by Cranfield University.

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.

no / Formal modelling is essential for precisely defining, understanding and reasoning when designing complex systems, such as cyberphysical systems. In this paper we present a formal specification using Event-B and Rodin platform for a case study of a cruise control system for a hybrid propulsion vehicle and electric bicycle (e-Bike). Our work uses the EventB method, a formal approach for reliable systems specification and verification, being supported by the Rodin platform, based on theorem proving, allowing a stepwise specification process based on refinement. We also use, from the same platform, the ProB model checker for the verification of the B-Machine and iUML plug-in to visualize our model. This approach shows the benefits of using a formal modelling platform, in the context of cyberphysical systems, which provides multiple ways of analysing a system. / Romanian National Authority for Scientific Research, CNCS-UEFISCDI, project number PN-III-P4-ID-PCE-20160210.

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.