Description
Date depot: 1 janvier 1900
Titre: Intégration de politiques de sécurité et de sûreté de fonctionnement pour la modèlisation, la vérification et la génération de systèmes critiques
Encadrant :
Jérôme HUGUES (LTCI (EDMH))
Directeur de thèse:
Laurent PAUTET (LTCI (EDMH))
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
1 Introduction
Le travail de thèse a lieu dans l’équipe S3 (System, Software and Services), au sein du département «
Informatique et Réseaux» de Telecom ParisTech.
S3 se compose actuellement de 8 enseignants-chercheurs permanents (dont 3 habilités à diriger des
recherches), 12 doctorants. L’équipe S3 s’intéresse à la modélisation, la conception et la vérification des
systèmes répartis et en particulier des systèmes Temps Réel Répartis Embarqués (TR2E).
Notre objectif est de développer des techniques de modélisation, des outils de vérification, des platesformes
d’exécution et des générateurs de code permettant à des ingénieurs de développer sans risque des
systèmes TR2E. En particulier, S3 a acquis une expertise reconnue internationalement dans l’architecture
d’intergiciels hautement configurables en fonction des propriétés requises par le système. Ces cinq dernières
années, S3 a également développé une forte compétence dans la modélisation et la génération automatique
des systèmes TR2E par le biais d’ADL et notamment d’AADL.
2 Contexte
L’usage des systèmes Temps Réel Répartis Embarqués (TR2E) s’est aujourd’hui généralisé, tant auprès
du grand public (téléphonie mobile, PDA, ...) qu’au sein de systèmes complexes (issus du domaine
aérospatial, automobile, énergétique).
Le recours à ces systèmes dans de nombreuses activités critiques (aéronautique, spatial, transport, médical,
bancaire) ajoute une contrainte forte en termes de sûreté de fonctionnement : une erreur peut avoir
un impact économique, industriel voire humain important. Il est donc crucial d’intégrer la sécurité et la
sûreté de fonctionnement au processus de construction de l’application afin d’évaluer et limiter tout risque
d’erreurs. Ceci passe autant par l’application d’éléments formels et théoriques (étude stochastique) que
techniques de conception (DO-178B, IMA, OMG DDS, MILS).
En parallèle, la complexité croissante du logiciel a conduit à la définition de couches d’abstraction et
de méthodes de conception. Ainsi l’industrie s’oriente vers des environnements de modélisation et des infrastructures
logicielles d’exécution à base de composants logiciels permettant d’améliorer le processus de
développement par le biais d’une rationalisation de la gestion de projet (réutilisation, intégration, maintenance
évolutive), d’une séparation entre les préoccupations fonctionnelles et celles purement techniques
(adaptation aux couches sous-jacentes, communication, auto-observation, intégrité ...), et d’un outillage
permettant de valider ou analyser le couple application/environnement d’exécution (évaluation des taux de
pannes, de l’ordonnancement, etc.).
Les environnements de modélisation et de conception ainsi que les intergiciels qui les accompagnent
doivent donc intégrer des préoccupations de vérification formelle des composants comme leur isolation en
fonction de leur niveau de sécurité ou de criticité.
3 Positionnement du travail
Le logiciel et son environnement d’exécution doivent fournir des éléments permettant de valider finement
son bon fonctionnement, dans des contextes où la certification (avionique) ou la validation (spatial)
sont cruciaux pour autoriser l’utilisation du système.
Se posent alors de multiples questions lors de la construction du couple logiciel/environnement d’exécution
: quelles sont les propriétés à tester ? Quelles sont les techniques de validation associées ? Quelles
sont les processus et les outils à mettre en oeuvre pour guider l’ingénieur dans ces choix de conception et
lors de la réalisation ?
La variété des besoins impose la définition d’un processus intégré reposant sur des standards, combinés
et intégrés et sa mise en oeuvre. La sécurité et la sûreté de fonctionnement imposent la définition de politiques,
leur validation (e.g. théorème de Bell-Lapadula) et leur mise en oeuvre dans le cadre de standards
(OMG DDS, RT-CORBA, ARINC 653, etc). La prise en compte simultanée de ces deux aspects pose pour
le moment de nombreux problèmes théoriques visant à terme la suppression des méthodes ad hoc employées
aujourd’hui et son remplacement par un processus fiable autorisant séparation des préoccupations, analyse
guidée, configuration de l’environnement d’exécution.
4 Problématique de la thèse
L’hétérogénéité des besoins tant théoriques que pratiques amène de nouveaux problèmes pour l’ingénierie
logicielle, qui doit pouvoir s’adapter à une large variété de théories (model checking classique, stochastique,
temporisé, preuves) et technologies (intergiciels, noyaux temps réel), sans pour autant en maîtriser
tous les aspects.
Il devient alors nécessaire d’abstraire l’architecture du système pour permettre son analyse, et la définition
de ces environnements. Une architecture comme celle proposée dans les specifications de MILS
permet d’effectuer des vérifications mathématiques (sur l’ordonnancement par exemple) en réduisant et isolant
de manière significative les portions de code critiques. La des
Doctorant.e: Lasnier Gilles