proposition de thèse : Ingénierie des modèles et méthodes formelles intégrées pour la concept

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