proposition de thèse : Ingénierie des modèles et méthodes formelles intégrées pour la conception de plates-formes embarquées dans un aéronef

Bonjour,
>
> Merci de faire circuler ce sujet de thèse pour lequel nous recherchons un
> candidat.
>
> Merci de candidater par mail. Envoyer lettre de motivation, CV,
> recommandation(s) à :
> pautet@telecom-paristech.fr
>
> Cette thèse se déroulerait en partenariat avec un industriel du domaine.
> Le sujet tel qu'il est envisagé actuellement par le partenaire serait le
> suivant.
>
> --
> Ingénierie des modèles et méthodes formelles intégrées pour la conception
> de plates-formes embarquées dans un aéronef
>
> Contexte
> Les systèmes embarqués avioniques civils vivent une mutation importante.
>
> Les architectures modulaires intégrées (IMA) déjà embarquées sur l'A380
> doivent pour les avions futurs répondrent à de nouvelles exigences de :
>
> * Réduction de complexité
>
> * Réduction de poids
>
> * Reconfiguration
>
> Le processus de conception des plates-formes IMA requiert des méthodes et
> outils innovants dès la phase de RAO, lors de la phase de JDP (Joint
> Definition Phase) avec l'avionneur jusqu'au développement du prototype
> afin d'aider à décrire et valider à chaque étape, l'architecture proposée
> vis à vis des besoins opérationnels multi- critères (fonctionnels, sureté
> de fonctionnement, MTBF (Mean Time Between Failure), sécurité).
>
> Le besoin de caractériser une plate-forme à partir de ses types de
> propriétés, de vérifier que ces propriétés seront respectées et de savoir
> le démontrer est motivé par :
>
> * La parallélisation du processus de conception/développement.
>
> * Les exigences de certification issues de la DO 178 / DO254 /DO297 /
> MILS-CC applicables à nos développements
>
>
> Problématique
> Des outils aidant à concevoir à travers des modèles, l'architecture, le
> paramétrage et la configuration de nos plate formes existent aujourd'hui,
> mais d'une part, ils fonctionnent sur des pré-requis qui imposent des
> concepts d'architectures et d'autre part définissent des règles empêchant
> leur intégration dans des environnements de modélisation plus larges.
>
> Notre problématique est aujourd'hui d'être capable de:
>
> 1. décrire dans un langage d'interchange des modèles (ou méta modèle)
> à composants hétérogènes (dont les propriétés sont parfaitement décrites
> par un langage formel)
>
> 2. animer un modèle par des stimuli représentatifs des
> caractéristiques des applications . Les stimuli doivent être bâtis comme
> des instances d'objets parfaitement décrits par un langage formel
>
> 3. produire des référentiels de performances (spécifiques ou
> génériques selon le type de stimuli)
>
> 4. vérifier (par les combinatoires appropriées ou par récursivité)
> les propriétés mises en jeu
>
> 5. démontrer que l'on a bien vérifié
>
> 6. générer automatiquement le code d'applications de référence
> (produisant un référentiel de performance de référence)
>
> --
> -- Laurent
>
>
>