Soutenance de thèse de Khaoula BOUKIR (équipe STR)
16 décembre 2020 @ 10 h 00 min - 12 h 30 min
Khaoula Boukir, doctorante au sein de l’équipe STR, soutiendra sa thèse intitulée « Mise en œuvre de politiques d’ordonnancement temps réel multiprocesseur prouvée » / « Proven implementation of multiprocessor real-time scheduling policies »
mercredi 16 décembre 2020 à 10h en visio.
Lien de connexion : https://univ-nantes-fr.zoom.us/j/86296772127?pwd=RXFzQU1lem9tQzFsQXMySFc4cjRaZz09 (Meeting ID: 862 9677 2127 / Passcode: 960277)
Jury :
– Directeur de thèse : Jean-Luc Béchennec, Chargé de recherche, CNRS
– Co-encadrant : Anne-Marie Déplanche, Maître de conférences, Université de Nantes
– Rapporteurs : Claire Pagetti Ingénieur recherche, ONERA ; Emmanuel Grolleau, Professeur des universités, ISAE-ENSMA
– Autres membres : Isabelle Puaut, Professeur des universités, Université de Rennes 1 ; Pascal Richard, Professeur des universités, Université de Poitiers ; Pierre-Emmanuel Hladik, Maître de conférences, INSA de Toulouse ; Olivier-Henri Roux, Professeur des universités, Centrale Nantes
Résumé : L’implémentation d’une nouvelle politique d’ordonnancement au sein d’un système d’exploitation temps réel n’est pas une tâche facile. Le passage de la spécification littéraire abstraite d’une politique à mise en oeuvre sur une plateforme réelle exige que des choix de réalisation soient faits et que des contraintes de diverses natures inhérentes à cette dernière soient prises en compte. Par conséquent, l’implémentation d’un ordonnanceur doit impérativement être accompagnée d’un travail de vérification permettant d’apporter un niveau de confiance en la validant la conformité du comportement de l’ordonnanceur implémenté par rapport à sa spécification d’origine.
Dans cette thèse, nous nous intéressons à l’utilisation des méthodes formelles pour la vérification des implémentations d’ordonnanceurs temps réel. Nous proposons une approche de vérification de type « model-checking », que nous conduisons sur des implémentations d’ordonnanceurs globaux menées au sein de Trampoline, un système d’exploitation temps réel conforme aux standardx OSEK/VDX et AUTOSAR. Pour chaque implémentation, un modèle décrivant son fonctionnement est élaboré avec des machines à états finis et temporisées. Ce modèle est stimulé par des générateurs produisant des scénarios indéterministes d’événements d’ordonnancement afin d’observer la réaction de l’implémentation à vérifier face à diverses situations. La vérification est alors menée en examinant la satisfaction d’une ensemble d’exigences spécifiées en fonction du comportement attendu de l’implémentation tel que stipulé dans la littérature. Cette approche a permis la vérification de la correction fonctionnelle du comportement de deux implémentations d’ordonnanceurs globaux dans Trampoline : G-EDF et EDF-US. Toutefois, son caractère modulaire et générique permet d’en envisager l’usage pour d’autres politiques et dans d’autres systèmes d’exploitation
Mots-clés : Politique d’ordonnancement temps réel, système d’exploitation temps réel, Implémentation d’ordonnancement, Model-checking
———————————————————————————————————————————————————
Abstract: Implementing a new scheduling policy within a real-time operating system is not an easy rask. Moving from an abstract literary specification of a policy to its implementation within a real platform requires making choices of realization and considering various contraints inherent to the latter. Consequently, a scheduler implementation work shall imperatively be supported by a verification study allowing to bring a level of confidence by validating the conformity of the behavior of the implemented scheduler compared to its original specification. In this thesis, we are interested in the use of formal methods for the verification of real-time scheduler implementations. We propose a « modelchecking » approach, which we conduct on global
scheduler implementations carried out on Trampoline, a real-time operating system compliant with OSEK/VDX and AUTOSAR standards. For each implementation, a model describing its behavior is elaborated with finite state and timed machines. This model is stimulated by generators producing indeterministic scenarios of scheduling events in order to observe the reaction of the implementation under various situations. The verification is then conducted by examining the satisfaction of a set of specified requirements according to the expected behavior of the implementation as stipulated in the literature.
This approach allowed the verification of the functional correction of the behavior of two implementations of global schedulers in Trampoline: G-EDF and EDF-US. However, its modular and generic character allows to consider its use for other policies and in other operating systems.
Keywords: Real-time scheduling policy, Real-time operating system, Scheduer implementation, Model-checking
