Détails sur le séminaire

Résumé : Cette thèse a été co-encadrée par le laboratoire MAPS/AMS de France Telecom R&D
(aujourd'hui MAPS/SHINE) et le laboratoire VERIMAG.
Le développement de logiciels pour les systèmes embarqués présente de nombreux
défis. Cette thèse s'intéresse à ceux posés par les interactions entre les
trois phases de conception (les développeurs construisent à partir de
spécifications un modèle du système exprimé dans un langage de conception
i.e. de programmation), d'implantation (le modèle précédent est compilé en un
exécutable du système qui est finalement déployé sur les plateformes réelles) et
de validation (un ensemble de techniques sont mises en oeuvre pour vérifier
que le système implanté est correct vis-à-vis des spécifications).
Pour cela nous nous intéressons aux caractéristiques du langage de conception et
aux techniques de compilation de ce langage. Celles-ci permettent d'obtenir dans
notre approche à la fois l'implantation du système et un modèle du système
implanté. L'analyse de ce modèle permet la validation de l'implantation, ce qui
suppose que ce modèle représente fidèlement le système implanté.
Nous proposons la construction d'un langage de conception basé sur l'utilisation
de composants logiciels prédéfinis dont le comportement dynamique est supposé
connu. Nous illustrons cette démarche par la réalisation d'un prototype complet
d'un langage appelé Buzz, inspiré des modèles de programmation à acteurs dans
lequel les composants logiciels utilisés sont des composants Think accompagnés
de leur modèle comportemental opérationnel constitué d'un composant BIP.
Le compilateur associé à Buzz que nous avons développé à partir du compilateur
Think existant (Nuptse) génère simultanément une architecture à composants
Think pour l'implantation et un modèle à composants BIP à des fins
d'analyse. Nous évaluons Buzz à travers deux expériences.
La première présente le développement de bout en bout d'un logiciel pour un
exemple académique sur lequel nous démontrons la pertinence des choix
techniques. Think nous permet un support d'implantation complet (compilation,
optimisation, déploiement) et BIP rend possible la vérification d'un ensemble de
propriétés dynamiques du système.
La deuxième expérience consiste à porter une application réelle de protocole
radio utilisée dans des réseaux de capteurs et développée de manière classique,
vers Buzz. Cette expérience démontre l'effectivité de notre proposition tant en
termes de langage de programmation (l'expressivité de Buzz structure et
simplifie le code original) qu'en termes d'outils de compilation et de
vérification.




Jury:
Président: STEFANI Jean-Bernard (INRIA)
Rapporteur: SEINTURIER Lionel (Univ. Lilles)
Rapporteur: MULLER Gilles (INRIA)
Directeur de thèse: SIFAKIS Joseph (VERIMAG)
Examinateur: PULOU Jacques (Orange Labs)
Examinateur: LE PAPE-GARDEUX Claude (Scheider Electrics)