Modélisation formelle de systèmes Insensibles à la Latence et ordonnancement.

This PhD thesis introduces new results linking the theory of Latency Insensitive, to a well-known sub-class of Petri Nets called Marked Event Graphs and its extension called Synchronous Data Flow. This work is tightly linked with a well-known problem, called Central Repetitive Problem (workshop scheduling...). We introduce the Synchronous Models, Marked Event Graphs, Synchronous Data Flow (SDF) and Latency Insensitive. After, we discuss existing links between the Synchronous Models, Marked Event Graphs, Synchronous Data Flow (SDF) and Latency Insensitive ; we show that the Latency Insensitive model is a special case of the Marked Event Graph model. After, we recall a well-known result : any Marked Event Graph with at least a strongly connected component (and evaluating with the firing rule As Soon As Possible (ASAP)) enjoys an ultimately repetitive behaviour : that is to say that it exists a static schedule. Starting from this result, we build a specific scheduling scheme called Equalization that is altering virtually the communication topology in order to slow-down too fast pathes adding some "registers", while preserving the global performance in throughput of the original system. Finally, we introduce some limited control in the Latency Insensitive Model, with nodes called select and merge where conditions are known and independant of data flows, more precisely datas are directed by ultimately periodic binary words (just like in the case of the static scheduling). We are creating then an abstraction over the SDF model in order to determinate if the instance of the model accepts a schedule where the size of each place in bounded. We can verify then the liveness of the system through simulation if the original system was having at least a strongly connected component. Finally, we conclude and discuss possibilities for future works.Cette thèse présente de nouveaux résultats liant la théorie des systèmes dits insensibles à la latence, à une sous-classe des réseaux de Pétri dénommée Marked Event Graph et son extension dite Synchronous Data Flow. Ces travaux sont intimement associés avec le problème d'ordonnancement général dénommé problème central répétitif. Nous introduisons les modèles synchrones, Marked Event Graphs, Synchronous Data Flow (SDF) et Latency Insensitive. Après, nous discutons des liens existants entre les modèles synchrones, Marked Event Graphs et Latency Insensitive ; nous montrons que le modèle Latency Insensitive est un cas particulier du modèle Marked Event Graph. Nous présentons ensuite une implémentation vérifiée formellement de Latency Insensitive. Après, nous rappelons un résultat connu : tout Marked Event Graph ayant au moins une partie fortement connexe (et s'évaluant avec une règle d'exécution As Soon As Possible (ASAP)) a un comportement ultimement répétitif : c'est à dire qu'il existe un ordonnancement statique. À partir de ce résultat, nous construisons une technique d'ordonnancement particulière dénommée Égalisation qui altère virtuellement la topologie des communications du système afin de ralentir des chemins trop rapides en rajoutant des "registres", tout en conservant les performances en terme de débit du système originel. Enfin, nous introduisons une notion de contrôle limité au modèle Latency Insensitive, avec des noeuds appelés select et merge dont les conditions sont connueset indépendantes des flots de données, plus exactement les conditions d'aiguillage des données sont dirigées par des mots binaires ultimement périodiques (comme dans le cadre de l'ordonnancement statique). Nous effectuons ensuite une abstraction sur le modèle SDF afin de déterminer si le modèle accepte un ordonnancement où la taille de toute place est bornée. Nous pouvons vérifier ensuite la vivacité du système grâce à une simulation, si le modèle originel disposait d'au moins d'une partie fortement connexe. Finalement, nous concluons et discutons des possibilités de travaux futurs