Soutenance de thèse de Imane HAUR

Imane HAUR, doctorante au sein de l’équipe STR, soutiendra sa thèse intitulée :

« Modélisation et vérification formelles d’un RTOS multicœur conforme à AUTOSAR »  / « AUTOSAR compliant multi-core RTOS formal modeling and verification »

le 30 novembre 2022, à 10h, dans l’amphithéâtre du bâtiment S, sur le campus de l’École Centrale. La présentation des travaux se fera en français.

Cette thèse a été préparée au sein du laboratoire LS2N à l’École Centrale de Nantes dans le cadre d’une thèse CIFRE avec le centre de recherche de Huawei Paris.

Jury :

• Directeur de thèse : Pr. Olivier H. ROUX
• Co-encadrant : Dr. Jean-Luc BÉCHENNEC (Chargé de recherche, CNRS)
• Rapporteurs : Pr. Emmanuel GROLLEAU (Professeur des universités, ISAE-ENSMA); Pr. Patrick MARTINEAU (Professeur des universités, École Polytechnique de l’Université de Tours).
• Autres membres : Pr. Gaétan HAINS (Professeur des universités, HUAWEI Paris research center); Pr. Isabelle PUAUT (Professeure des universités, Université de Rennes).

Résumé : La vérification formelle est une solution pour augmenter la fiabilité de l’implémentation du système.
Dans notre travail de thèse, nous nous intéressons à l’utilisation de ces méthodes pour la vérification des systèmes d’exploitation multi-cœurs temps réel. Nous proposons une approche de model-checking utilisant les réseaux de Petri temporels, étendus avec des transitions colorées et des fonctionnalités de haut niveau. Nous utilisons ce formalisme pour modéliser le système d’exploitation multi-cœur Trampoline, conforme aux standards OSEK et AUTOSAR. Nous définissons dans un premier temps ce formalisme et montrons son adéquation avec la modélisation de systèmes concurrents temps reel. Nous utilisons ensuite ce formalisme pour modéliser le système d’exploitation multi-cœur Trampoline et vérifions par model-checking sa conformité avec le standard AUTOSAR. À partir de ce modèle, nous pouvons vérifier des propriétés aussi bien sur l’OS que sur l’application telles que l’ordonnançabilité d’un système temps-réel ainsi que les mécanismes de synchronisation : accès concurrents aux structures de données du système d’exploitation, ordonnancement multi-cœur et traitement des interruptions inter-cœur. À titre d’illustration, cette méthode a permis l’identification automatique de deux erreurs possibles de l’OS Trampoline dans l’exécution concurrente, montrant une protection insuffisante des données et une synchronisation défectueuse.

Mots-clés : Vérification formelle, Model-checking, Réseaux de Petri colorés de haut niveau, Systèmes d’exploitation temps réel, Exécution multi-cœurs, Vérification d’OS AUTOSAR.

Abstract: Formal verification is a solution to increase the system’s implementation reliability. In our thesis work, we are interested in using these methods to verify multi-core RTOS. We propose a model-checking approach using time Petri nets extended with colored transitions and high-level features. We use this formalism to model the Trampoline multi-core OS, compliant with the OSEK and AUTOSAR standards. We first define this formalism and show its suitability for modeling real-time concurrent systems. We then use this formalism to model the Trampoline multi-core RTOS and verify by model-checking its conformity with the AUTOSAR standard. From this model, we can verify properties of both the OS and the application, such as the schedulability of a real-time system and the synchronization mechanisms: concurrent access to the data structures of the OS, multi-core scheduling, and inter-core interrupt handling. As an illustration, this method allowed the automatic identification of two possible errors of the Trampoline OS in concurrent execution, showing insufficient data protection and faulty synchronization.

Keywords: Formal verification, Model-checking, High-level Colored Time Petri Nets, Real-Time Operating Systems (RTOS), Multi-core execution, AUTOSAR OS verification.