Modeling, evaluation and validation of distributed real time systems.

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