Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-01224465
Contributor : Stephan Merz <>
Submitted on : Wednesday, November 4, 2015 - 4:22:47 PM
Last modification on : Friday, November 13, 2020 - 3:22:08 PM
Long-term archiving on: : Friday, February 5, 2016 - 11:18:35 AM

File

paper 34.pdf
Files produced by the author(s)

Identifiers

  • 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. Modélisation des Systèmes Réactifs (MSR 2015), Nov 2015, Nancy, France. ⟨hal-01224465⟩

Share

Metrics

Record views

441

Files downloads

180