Soutenance de Thèse de Xavier Renault

Bonjour à tous,

J'ai le plaisir de vous inviter à ma soutenance de thèse de doctorat
intitulée :

"Mise en oeuvre de notations standardisées, formelles et semi-
formelles dans un processus de développement de systèmes embarqués
temps-réel répartis."

La soutenance se déroulera le 3 décembre 2009, à 14h dans les locaux
du LIP6 :

salle 549
104 avenue du Président Kennedy
75016 Paris

Vous êtes également conviés au pot qui suivra.

Pour les visiteurs extérieurs au LIP6, veuillez penser à vous munir
d'une pièce d'identité.

Résumé :

Dans un processus d'ingénierie dirigée par les modèles (IDM),
l'ingénieur modélise son système à l'aide d'une notation semi-
formelle, le valide puis l'implante. L'étape de validation est
cruciale pour les systèmes temps-réel répartis et embarqués (TR2E),
pour s'assurer de leur bon fonctionnement logique ou temporel.
Cependant, une démarche IDM n'est pas suffisante car elle n'indique
pas comment utiliser les modèles pour faire des analyses. Il est
nécessaire d'adopter une démarche d'Ingénierie Dirigée par les
Vérifications et les Validations (IDV2) pour s'assurer que le système
est correctement construit, et qu'il satisfait un ensemble de
propriétés spécifiées en amont dans le processus de développement.

Cette thèse propose un processus de développement, de validation et de
vérification basé sur des notations formelles, et dédié aux
applications TR2E. Le langage AADL (Architecture Analysis and Design
Language) est utilisé comme notation pivot. Le processus proposé prend
en compte les aspects comportementaux de l'application et les aspects
architecturaux de l'exécutif. Il repose sur des notations
standardisées, pour faire face aux problèmes d'interopérabilités des
outils mis en oeuvre.

Notre démarche permet d'obtenir des retours aussi bien à propos de
l'applicatif que de l'exécutif, et permet de corriger ou modifier les
modèles dans un processus de développement itératif. Au cours de
notre démarche, nous transformons les spécifications AADL vers
différentes notations standardisées : les réseaux de Petri pour la
validation de l'applicatif, la notation Z pour la vérification de
l'exécutif utilisé, PolyORB.

Jury :

Laurence Duchien Rapporteur Professeur à l'Université de Lille 1
Michel Lemoine Rapporteur Directeur de recherche à l'ONERA CMP

Béatrice Bérard Examinateur Professeur à l'Université Pierre et
Marie Curie
Peter Feiler Examinateur Senior Technical Staff - Carnegie Mellon
University, SEI
Laure Petrucci Examinateur Professeur à l'Université de Paris 13

Jérôme Hugues Encadrant Maître de Conférences à l'ISAE
Fabrice Kordon Directeur Professeur à l'Université Pierre et Marie
Curie

--
Xavier Renault
LIP6