Approche formelle pour la spécialisation de systèmes d'exploitation temps réel

Résumé : Le développement d'un système d'exploitation spécialisé pour une application consiste, à partir du code d'un système d'exploitation complet, à l'élaguer pour l'adapter aux fonctionnalités nécessaires à l'application. L'opération d'élagage est réalisée à la main au cas par cas. Cela rend très difficile la vérification et la certification d'un système d'exploitation car non seulement la phase de certification est à réaliser pour chaque spécialisation mais aussi le problème difficile et bien connu du fossé entre le modèle utilisé pour la vérification et le code est à étudier au cas par cas. Dans cet article, nous proposons une méthode pour l'automatisation complète de cet élagage au moyen d'une synthèse du système d'exploitation à partir d'un modèle formel embarquant le code du système d'exploitation. Ce modèle comporte en effet à la fois le flot de contrôle, les variables du système d'exploitation et les séquences d'instructions manipulant ces variables. L'élagage, formalisé par l'élimination des chemins infaisables du modèle, permet de ne conserver que la partie accessible (et donc utile) du modèle et donc du code. Cette méthode, non seulement accélère considérablement l'adaptation du système d'exploitation mais, de plus, garantit l'optimalité du code généré et l'absence de code mort. La vérification et la certification de toutes les fonctionnalités souhaitées du système d'exploitation comme l'absence de blocage, peuvent être également réalisées sur le modèle avant la génération de code. Nous utilisons un modèle du système d'exploitation temps réel Trampoline compatible OSEK et AUTOSAR, qui est reconnu comme fiable et largement utilisé aux niveaux académique et industriel.
Type de document :
Communication dans un congrès
Stephan Merz and Jean-François Pétin. Modélisation des Systèmes Réactifs (MSR 2015), Nov 2015, Nancy, France
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01224465
Contributeur : Stephan Merz <>
Soumis le : mercredi 4 novembre 2015 - 16:22:47
Dernière modification le : jeudi 15 mars 2018 - 14:28:04
Document(s) archivé(s) le : vendredi 5 février 2016 - 11:18:35

Fichier

paper 34.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01224465, version 1

Collections

Citation

Kabland Toussaint Gautier Tigori, Jean-Luc Béchennec, Olivier Henri Roux. Approche formelle pour la spécialisation de systèmes d'exploitation temps réel. Stephan Merz and Jean-François Pétin. Modélisation des Systèmes Réactifs (MSR 2015), Nov 2015, Nancy, France. 〈hal-01224465〉

Partager

Métriques

Consultations de la notice

315

Téléchargements de fichiers

93