AUTOSAR compliant multi-core RTOS formal modeling and verification

La vérification formelle est une solution pour augmenter la fiabilité de l’implémentation du système. Dans ce travail, 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 réel. Nous utilisons ensuite ce formalisme pour modéliser le système d’exploitation multi-cœur Trampoline et vérifions par model-checking. À 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.