• Media type: Text; E-Book; Electronic Thesis
  • Title: Allocation sûre dans les systèmes aéronautiques : modélisation, vérification et génération
  • Contributor: Sagaspe, Laurent [Author]
  • imprint: theses.fr, 2008-12-04
  • Language: French
  • Keywords: AltaRica ; Sûreté de fonctionnement ; Aéronautique ; Systèmes embarqués ; Méthodes formelles
  • Origination:
  • Footnote: Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
  • Description: Les architectures des systèmes embarqués des nouvelles générations d'avions civils et militaires tendent à s'organiser autour d'une plateforme avionique constituée de calculateurs interconnectés par un réseau central. Ce type d'architecture a fait apparaitre le besoin de développer de nouvelles méthodes de conception afin d'assister le dialogue entre les concepteurs des fonctions à embarquer (commandes de vol, gestion de l'énergie, .) et les architectes de la plateforme avionique. Il est, en particulier, primordial de s'assurer que l'allocation des ressources de la plateforme aux fonctions embarquées respecte les exigences de sûreté de fonctionnement propres aux systèmes avioniques. Dans un premier temps, un cadre général a été proposé pour modéliser et vérifier l'effet de l'allocation des ressources d'une plateforme avionique du point de la sûreté de fonctionnement. Ce cadre est fondé sur l'utilisation du langage AltaRica pour décrire formellement la propagation des défaillances au sein de systèmes embarqués et des outils associés à ce langage (model-checking, génération de séquences et d'arbres de défaillances) pour vérifier la tenue des exigences de sûreté de fonctionnement. Ce cadre a été utilisé pour étudier, d'une part, l'allocation d'équipements informatiques aux fonctions de systèmes embarqués, et d'autre part, les placements des équipements au sein de l'avion en tenant compte de risques tels que l'éclatement d'un pneu ou l'explosion d'un moteur. Dans un second temps, la génération d'allocations respectant les exigences de sûreté de fonctionnement a été étudiée. L'approche retenue est fondée sur l'expression de contraintes d'allocation sous forme d'inégalités linéaires entières et sur l'utilisation de techniques de résolution de ces contraintes. Plusieurs types de contraintes (ségrégation, co-location, exclusion, .) sont pris en compte. De plus, des critères d'optimisation permettent de guider la résolution des contraintes de façon à proposer des allocations les plus pertinentes du point de vue des ...
  • Access State: Open Access