Modélisation et Analyse de Systèmes Temps Réel avec Préemption, Incertitude et Dépendence

Dominique Duval - presidente Jacques Pilou - Examinateur Philippe Clauss - Examinateur Ahmed Bouajjani - Rapporteur Alfredo Olivero - RapporteurWe consider scheduling real time systems. We give a model for a special class of real time programs, based on dependencies (shared resources and communications). We analyse this model and give a fixed priority assignment algorithm with a detection technique to treat deadlock. We extend this approach and give a real time model based on timed automata. We propose some techniques to deal with the problem of schedulability based on some policies such as LIFO, EDF and a General Preemptive Policy. For each model, we prove the decidability of the scheduler through the resolution of its corresponding reachability problem.On considère le problème d'ordonnancement des systèmes temps-réel. On commence par la modelisation d'une certaine classe de programmes Java, avec des processus concurrents constitués d'une séquence de tâches temps-réel qui se synchronisent et peuvent accéder aux ressources communes. Pour ce modèle on analyse l'ordonnancement en proposant un algorithme d'attribution de priorités fixes; le problème de deadlock est aussi analysé grace à une technique de détection. A partir de ce problème, on aborde l'ordonnancement dans une approache plus générale basée sur le modèle des automates temporsés; on propose de techniques pour décider le problème d'ordonnancement qui réposent sur des procédures d'analyse symbolique d'accessibilité dans differents modèles: LIFO one-préemption, EDF one-préemption, General Scheduling. Pour chaque modèle on donne une serie de proprietés, notamment la preuve d'accessibilité. On conclut par donner une methode complète d'ordonnancemen