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
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 Télécom 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é.
Cette thèse s’intègre dans les travaux menés dans le contexte du projet PARSEC. A titre indicatif, nous
rappelons l’objet de celui-ci.
Le projet PARSEC vise à définir un atelier de développement des systèmes temps-réel embarqués distribués
critiques qui nécessitent une certification selon les standards les plus stricts tels que les normes
DO-178B (avionique), IEC 61508 (transports), ou les Critères Communs pour l’évaluation de la Sécurité
des Systèmes d’Information (Sécurité des systèmes d’information).
La démarche poursuivie par PARSEC a pour but de fournir aux ingénieurs en charge de ces systèmes
une suite d’outils intégrée pour répondre aux contraintes de certification des systèmes embarqués. En l’occurrence,
ces systèmes doivent :
– être rigoureusement spécifiés - PARSEC s’appuiera sur l’approche B événementielle pour aboutir à
un modèle prouvé de l’attendu du système.
– être rigoureusement conçus - PARSEC offrira alors les moyens de décliner cet attendu en un modèle
de composants (technologie MyCCM High Integrity) décrivant l’application et ses paramètres nonfonctionnels
(caractéristiques temps réel, projection sur une plate-forme partitionnée notamment).
– être rigoureusement implantés - PARSEC définira des générateurs pour le code correct par construction
pour l’assemblage et le contrôle des composants logiciels, en suivant d’une part une approche
synchrone (technologie SynDEx) et d’autre part une approche asynchrone (technologie Ocarina). Les
deux approches ont des applications différentes (implantation de lois de pilotage ou de protocoles de
radiocommunications, par exemple).
– être rigoureusement évalués (remontée du cycle en V) - PARSEC intégrera l’outil PathCrawler de
génération de scénarios de tests et définira un outil de traçabilité d’exigences.
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 autor
Doctorant.e: Cadoret Fabien