L'importance des systèmes temps-réels embarqués dans les sociétés industrialisées modernes en font un terrain d'application privilégié pour les méthodes formelles. La prépondérance des contraintes temporelles dans les spécifications de ces systèmes motive la mise au point de solutions spécifiques. Cette thèse s'intéresse à une classe de systèmes temps-réels incluant ceux développés avec la chaîne d'outils OASIS, développée au CEA LIST. Nos travaux portent sur la notion de délai de bout-en-bout, que nous proposons de modéliser comme une contrainte temporelle concernant l'influence du flot d'informations des entrées sur celui des sorties. Afin de répondre à la complexité croissante des systèmes temps-réels, nous étudions l'applicabilité de cette notion nouvelle au développement incrémental par raffinement et par composition. Le raffinement est abordé sous l'angle de la conservation de propriétés garantes de la correction du système au cours du processus de développement. Nous délimitons les conditions nécessaires et suffisantes à la conservation du délai de bout-en-bout lors d'un tel processus. De même, nous donnons des conditions suffisantes pour permettre le calcul du délai de bout-en-bout de manière compositionnelle. Combinés, ces résultats permettent d'établir un formalisme permettant la preuve du délai de bout-en-bout lors d'une démarche de développement incrémentale.

Dans cette thèse, nous proposons une nouvelle approche pour modéliser et estimer les délais de bout-en-bout dans les réseaux de capteurs sans-fil (WSN). Notre approche combine les approches analytiques et expérimentales pour inférer un modèle Markovien modélisant le comportement d'un protocole de contrôle d'accès au médium (MAC) exécuté sur les nœuds d'un réseau de capteurs. À partir de ce modèle Markovien, le délai de bout en bout est ensuite obtenu par une approche analytique basée sur une analyse dans le domaine fréquentiel pour calculer la probabilité de distribution de délais pour un taux d'arrivée spécifique. Afin d’obtenir une estimation du délai de bout en bout, indépendamment du trafic en entrée, la technique de régression non-linéaire est utilisée sur un ensemble d’échantillons limités. Cette approche nous a permis de contourner deux problèmes: 1) la difficulté d'obtenir un modèle Markovien du comportement d’un protocole MAC en tenant compte de son implémentation réelle, 2) l'estimation du délai de bout-en-bout d’un WSN multi-sauts. L'approche a été validée sur un testbed réel (IOT-LAB) et pour plusieurs protocoles (X-MAC, ContikiMAC, IEEE 802.15.4) ainsi que pour un protocole de routage (RPL). / In this thesis, we propose an approach that combines both measurements and analytical approaches for infering a Markov chain model from the MAC protocol execution traces in order to be able to estimate the end to end delay in multi-hop transmission scenarios. This approach allows capturing the main features of WSN. Hence, a suitable Markov chain for modelling the WSN is infered. By means of an approach based on frequency domain analysis, end to end delay distribution for multi-hop scenarios is found. This is an important contribution of our approach with regard to existing analytical approaches where the extension of these models for considering multi-hop scenarios is not possible due to the fact that the arrival distribution to intermediate nodes is not known. Since local delay distribution for each node is obtained by analysing the MAC protocol execution traces for a given traffic scenario, the obtained model (and therefore, the whole end to end delay distribution) is traffic-dependant. In order to overcome this problem, we have proposed an approach based on non-linear regression techniques for generalising our approach in terms of the traffic rate. Results were validated for different MAC protocols (X-MAC, ContikiMAC, IEEE 802.15.4) as well as a well-known routing protocol (RPL) over real test-beds (IOT-LAB).

Depuis l'avènement du réseau Internet, le volume de données échangées sur les réseaux a crû de manière exponentielle. Le matériel présent sur les réseaux est devenu très hétérogène, dû entre autres à la multiplication des "middleboxes" (parefeux, routeurs NAT, serveurs VPN, proxy, etc.). Les algorithmes exécutés sur les équipements réseaux (routage, “spanning tree”, etc.) sont souvent complexes, parfois fermés et propriétaires et les interfaces de supervision peuvent être très différentes d'un constructeur/équipement à un autre. Ces différents facteurs rendent la compréhension et le fonctionnement du réseau complexe. Cela a motivé la définition d'un nouveau paradigme réseaux afin de simplifier la conception et la gestion des réseaux : le SDN (“Software-defined Networking”). Il introduit la notion de contrôleur, qui est un équipement qui a pour rôle de contrôler les équipements du plan de données. Le concept SDN sépare donc le plan de données chargés de l'acheminement des paquets, qui est opéré par des équipements nommés virtual switches dans la terminologie SDN, et le plan contrôle, en charge de toutes les décisions, et qui est donc effectué par le contrôleur SDN. Pour permettre au contrôleur de prendre ses décisions, il doit disposer d'une vue globale du réseau. En plus de la topologie et de la capacité des liens, des critères de performances comme le délai, le taux de pertes, la bande passante disponible, peuvent être pris en compte. Cette connaissance peut permettre par exemple un routage multi-classes, ou/et garantir des niveaux de qualité de service. Les contributions de cette thèse portent sur la proposition d'algorithmes permettant à une entité centralisée, et en particulier à un contrôleur dans un cadre SDN, d'obtenir des estimations fiables du délai de bout-en-bout pour les flux traversant le réseau. Les méthodes proposées sont passives, c'est-à-dire qu'elles ne génèrent aucun trafic supplémentaire. Nous nous intéressons tout particulièrement à la moyenne et l'écart type du délai. Il apparaît que le premier moment peut être obtenu assez facilement. Au contraire, la corrélation qui apparaît dans les temps d'attentes des noeuds du réseau rend l'estimation de l'écart type beaucoup plus complexe. Nous montrons que les méthodes développées sont capables de capturer les corrélations des délais dans les différents noeuds et d'offrir des estimations précises de l'écart type. Ces résultats sont validés par simulations où nous considérons un large éventail de scénarios permettant de valider nos algorithmes dans différents contextes d'utilisation / Since the early beginning of Internet, the amount of data exchanged over the networks has exponentially grown. The devices deployed on the networks are very heterogeneous, because of the growing presence of middleboxes (e.g., firewalls, NAT routers, VPN servers, proxy). The algorithms run on the networking devices (e.g., routing, spanning tree) are often complex, closed, and proprietary while the interfaces to access these devices typically vary from one manufacturer to the other. All these factors tend to hinder the understanding and the management of networks. Therefore a new paradigm has been introduced to ease the design and the management of networks, namely, the SDN (Software-defined Networking). In particular, SDN defines a new entity, the controller that is in charge of controlling the devices belonging to the data plane. Thus, in a SDN-network, the data plane, which is handled by networking devices called virtual switches, and the control plane, which takes the decisions and executed by the controller, are separated. In order to let the controller take its decisions, it must have a global view on the network. This includes the topology of the network and its links capacity, along with other possible performance metrics such delays, loss rates, and available bandwidths. This knowledge can enable a multi-class routing, or help guarantee levels of Quality of Service. The contributions of this thesis are new algorithms that allow a centralized entity, such as the controller in an SDN network, to accurately estimate the end-to-end delay for a given flow in its network. The proposed methods are passive in the sense that they do not require any additional traffic to be run. More precisely, we study the expectation and the standard deviation of the delay. We show how the first moment can be easily computed. On the other hand, estimating the standard deviation is much more complex because of the correlations existing between the different waiting times. We show that the proposed methods are able to capture these correlations between delays and thus providing accurate estimations of the standard deviation of the end-to-end delay. Simulations that cover a large range of possible scenariosvalidate these results

L’importance des systèmes temps-réels embarqués dans les sociétés industrialisées modernes en font un terrain d’application privilégié pour les méthodes formelles. La prépondérance des contraintes temporelles dans les spécifications de ces systèmes motive la mise au point de solutions spécifiques. Cette thèse s’intéresse à une classe de systèmes temps-réels incluant ceux développés avec la chaîne d’outils OASIS, développée au CEA LIST. Nos travaux portent sur la notion de délai de bout-en-bout, que nous proposons de modéliser comme une contrainte temporelle concernant l’influence du flot d’informations des entrées sur celui des sorties. Afin de répondre à la complexité croissante des systèmes temps-réels, nous étudions l’applicabilité de cette notion nouvelle au développement incrémental par raffinement et par composition. Le raffinement est abordé sous l’angle de la conservation de propriétés garantes de la correction du système au cours du processus de développement. Nous délimitons les conditions nécessaires et suffisantes à la conservation du délai de bout-en-bout lors d’un tel processus. De même, nous donnons des conditions suffisantes pour permettre le calcul du délai de bout-en-bout de manière compositionnelle. Combinés, ces résultats permettent d’établir un formalisme permettant la preuve du délai de bout-en-bout lors d’une démarche de développement incrémentale. / Real-time embedded systems are at the core of modern industrialized societies. They are a privileged target for the application of formal methods. The importance of real-time constraints in the specification of these systems requires the design of ad-hoc solutions. This work considers a class of real-time systems including those developed using OASIS, a tool-chain targeting hard real-time embedded systems developed at CEA LIST. We study the notion of end-to-end delay, which we propose to model as a constraint bearing directly on the influence of the input information flow over the output information flow . In order to cope with the growing complexity of real-time embedded systems, we study the possibility to apply this new notion of delay to the incremental development of such systems, by using both stepwise refinement and composition operators. We define the necessary and sufficient conditions to the preservation of the end-to-end delay by stepwise refinement. Similarly, we give sufficient conditions to compute the end-to-end delay in a compositional fashion. Together, these results permit to establish a formalism allowing to prove end-to-end delay properties in stepwise development methodologies.

Dans cette thèse, nous analysons les réseaux des systèmes temps-réel distribués et plus particulièrement ceux des domaines de l’avionique et de l’automobile. Nous nous sommes focalisés sur deux protocoles : « Avionic Full DupleX Switched Ethernet » (AFDX), « Audio Vidéo Bridging Ethernet » (AVB). Dans ces domaines critiques, le déterminisme du réseau doit être garanti. Il consiste, notamment, en la détermination d’une borne garantie du délai de bout en bout de traversée du réseau pour chaque trame ; et un dimensionnement des files d’attente des trames suffisamment grand pour garantir qu’aucune d’entre elle ne débordera et ainsi, éviter toute perte de trame.Il existe plusieurs méthodes pour l’évaluation des délais et nous avons, principalement, travaillé sur la méthode « Forward end-to-end delay Analysis » (FA). FA avait déjà été définie avec la politique d’ordonnancement « First-In-First-Out » dans le contexte de l’AFDX. Nous sommes repartis de cette approche, nous l’avons reformulé et généralisé à n’importe quel réseau Ethernet commuté. Nous l’avons aussi étendu aux priorités statiques et au protocole AVB et sa politique de service « Credit Based Shaper ». Pour chaque contribution, des démonstrations formelles ont été présentées et une expérimentation incluant une comparaison de FA avec les principales approches d’évaluation sur un exemple industriel. Finalement, nous avons développé et démontré formellement une approche pour le dimensionnement des files d’attente en termes de nombre de trames. Cette approche a été expérimentée également sur une configuration industrielle. / In this thesis, we analyze networks in the context of distributed real-time systems, especially in the fields of avionics, with “Avionics Full DupleX Switched Ethernet” (AFDX), and automobile, with “Audio Video Bridging Ethernet” (AVB). For such applications, network determinism needs to be guaranteed. It involves, in particular, assessing a guaranteed bound on the end-to-end traversal time across the network fr each frame; and dimensioning the buffers in order to avoid any loss of frame because of a buffer overflow.There are several methods for worst-case delay analysis, and we have mainly worked on the “Forward end-to-end Delay Analysis” (FA) method. FA had already been developed for “First-In-First-Out” scheduling policy in the AFDX context, so we generalized it to any Switched Ethernet network. We have also extended it to handle static priorities and the AVB protocol, shaping policy named “Credit Based Shaper” (CBS). Each contribution has been formaly proved and experiments have been led on industrial configurations. For our experimentations, we have compared our results with the results of competing approaches. Finally, we have developed and formally demonstrated an approach for buffer dimensioning in terms of number of frames. This approach has also been tested on an industrial configuration and has produced tight bounds.

Tout comportement défectueux d’un système temps-réel critique, comme celui utilisé dans le réseau avionique ou le secteur nucléaire, peut mettre en danger des vies. Par conséquent, la vérification et validation de ces systèmes est indispensable avant leurs déploiements. En fait, les autorités de sécurité demandent d’assurer des garanties déterministes. Dans cette thèse, nous nous intéressons à obtenir des garanties temporelles, en particulier nous avons besoin de prouver que le temps de réponse de bout-en-bout de chaque flux présent dans le réseau est borné. Ce sujet a été abordé durant de nombreuses années et plusieurs approches ont été développées. Après une brève comparaison entre les différentes approches existantes, une semble être un bon candidat. Elle s’appelle l’approche par trajectoire; cette méthode utilise les résultats établis par la théorie de l'ordonnancement afin de calculer une limite supérieure. En réalité, la surestimation de la borne calculée peut entrainer la rejection de certification du réseau. Ainsi une première partie du travail consiste à détecter les sources de pessimisme de l’approche adoptée. Dans le cadre d’un ordonnancement FIFO, les termes ajoutant du pessimisme à la borne calculée ont été identifiés. Cependant, comme les autres méthodes, l’approche par trajectoire souffre du problème de passage à l’échelle. En fait, l’approche doit être appliquée sur un réseau composé d’une centaine de commutateur et d’un nombre de flux qui dépasse les milliers. Ainsi, il est important qu’elle soit en mesure d'offrir des résultats dans un délai acceptable. La première étape consiste à identifier, dans le cas d’un ordonnancement FIFO, les termes conduisant à un temps de calcul important. L'analyse montre que la complexité du calcul est due à un processus récursif et itératif. Ensuite, en se basant toujours sur l’approche par trajectoire, nous proposons de calculer une limite supérieure dans un intervalle de temps réduit et sans perte significative de précision. C'est ce qu'on appelle l'approche par trajectoire scalable. Un outil a été développé permettant de comparer les résultats obtenus par l’approche par trajectoire et notre proposition. Après application sur un réseau de taille réduite (composé de 10 commutateurs), les résultats de simulations montrent que la durée totale nécessaire pour calculer les bornes des milles flux a été réduite de plusieurs jours à une dizaine de secondes. / In critical real-time systems, any faulty behavior may endanger lives. Hence, system verification and validation is essential before their deployment. In fact, safety authorities ask to ensure deterministic guarantees. In this thesis, we are interested in offering temporal guarantees; in particular we need to prove that the end-to-end response time of every flow present in the network is bounded. This subject has been addressed for many years and several approaches have been developed. After a brief comparison between the existing approaches, the Trajectory Approach sounded like a good candidate due to the tightness of its offered bound. This method uses results established by the scheduling theory to derive an upper bound. The reasons leading to a pessimistic upper bound are investigated. Moreover, since the method must be applied on large networks, it is important to be able to give results in an acceptable time frame. Hence, a study of the method’s scalability was carried out. Analysis shows that the complexity of the computation is due to a recursive and iterative processes. As the number of flows and switches increase, the total runtime required to compute the upper bound of every flow present in the network understudy grows rapidly. While based on the concept of the Trajectory Approach, we propose to compute an upper bound in a reduced time frame and without significant loss in its precision. It is called the Scalable Trajectory Approach. After applying it to a network, simulation results show that the total runtime was reduced from several days to a dozen seconds.