Description
Date depot: 1 janvier 1900
Titre: Vérification compositionnelle pour la Conception sûre de systèmes embarqués
Directrice de thèse:
Emmanuelle ENCRENAZ (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
**Contexte**
Les systèmes embarqués sont bien implantés dans la vie courante. On les retrouve dans toute l'électronique de loisir grand public, mais également dans de nombreux domaines d'applications critiques : l'assistance opératoire et le diagnostic médical, l'automobile (une automobile de moyenne gamme comprend plus d'une vingtaine de controleurs répartis sur le véhicule), le transport ferroviaire ou aérien, .... Ces systèmes embarqués correspondent à l'intégration sur un même circuit, d'un ensemble de fonctionnalités complexes, réalisées par un très grand nombre de composants hétérogènes. Les systèmes sur puce actuels comprennent plusieurs processeurs exécutant de multiples tâches coopératives, des coprocesseurs spécialisés (pour des traitements applicatifs, ou pour les communication réseau), des composants radio-fréquences.
Ces systèmes sont fréquemment soumis à des impératifs de sûreté et de fiabilité. Selon leur domaine d'utilisation, leur défaillance peut causer de graves dommages. Il est important de pouvoir s'assurer, lors de leur conception, de leur correction vis-à-vis de leur fonctionalité. Du fait de leur très grande complexité, les méthodes de vérification actuelles ne permettent de vérifier que très partiellement ces systèmes.
Les méthodes de validation des systèmes complexes actuellement utilisées reposent presque exclusivement sur le test (fonctionnel), qui n'est pas exhaustif. Les méthodes de vérification automatiques, basées sur l'exploration de l'espace d'état du système (méthodes de vérification par modèle), sont appliquées pour certaines phases bien identifiées du processus de conception des systèmes embarqués, mais force est de reconnaitre que leur emploi reste marginal.
Un vérificateur de modèle (ou model-checker) est un programme qui détermine automatiquement si une propriété est vraie ou non pour un système fini donné. Le système fini est décrit comme une collection d’automates synchrones, représenté par une fonction de transition globale indiquant l’état du système à l’instant i+1 en fonction de son état à l’instant i, et la propriété caractérise un ensemble de comportements du système (désirables ou non), exprimée dans une logique temporelle (ici CTL). Les vérificateurs de modèle explorent le graphe des états du système (en utilisant l’état initial et la relation de transition) pour s’assurer que les comportements décrits par la propriété sont présents ou non dans le graphe. En général, les vérifications ne sont pas faites en parcourant les états un à un (il y en a trop), mais en parcourant simultanément des ensembles d’états, représentés symboliquement par leurs fonctions caractéristiques ; On parle de vérification de modèle symbolique. La représentation symbolique la plus utilisée est basée sur les diagrammes de décision binaire [McMillan 93]. Malgré les avancées apportées par cette représentation, les systèmes vérifiables restent de moyenne complexité. Une approche complémentaire consiste à adopter une démarche compositionnelle : on cherche à tirer partie de la structure en composants du système et de la propriété à vérifier, afin de réduire la taille de la représentation symbolique de l’espace d’états, et repousser ainsi les limites de la vérification par modèle.
Le département ALSOC du LIP6 a proposé et automatisé une méthode d’abstraction de composants, basée sur l’ensemble des propriétés que vérifie chaque composant [Braunstein 07] [Bara 08]. On souhaite l'intégrer dans une démarche plus générale de Raffinement d’Abstraction Guidée par le Contre-Exemple (CEGAR, [Clarke00]) qui est maintenant bien implantée pour la vérification de programmes C ou JAVA. Par exemple, les outils SLAM ou BLAST, et tout récemment VCEGAR [VCEGAR 07] offrent des possibilités de vérification très intéressantes pour des programmes de moyenne complexité.
**Objectifs de la thèse**
L’objectif de la thèse est de définir et implanter une méthode de vérification compositionnelle automatique, en s'appuyant sur :
la démarche de conception modulaire, dans laquelle chaque composant est défini, spécifié et vérifié avant d'être intégré dans un système plus complexe),
la démarche de vérification par abstraction CEGAR, qui permet de repousser les limites de la vérification par modèle en éliminant les variables du systèmes non pertinentes pour la vérification de telle ou telle propriété.
L'originalité de cette approche réside en la combinaison de ces deux démarches pour fixer un cadre de conception précis et rigoureux, qui s'inscrit dans une démarche qualité. La conception et la vérification sont intimement couplées : la formalisation de la spécification de chaque composant est nécessaire, et une fois chaque composant vérifié, cette spécification est utilisée pour simplifier la vérification de systèmes composés.
Cette démarche sera appliquée à plusieurs cas d'étude, représentant notamment des parties de systèmes embarqués provenant du domaine de l'automobile ou du traitem
Doctorant.e: Syed Alwi Syed Hussein