| Nom du Projet : (maximum 20 caractères) |
| SURE-PATHS |
| Titre du Projet : (maximum 3 lignes) |
| Evaluation stochastique de la fiabilité, de la performabilité et de la sureté de fonctionnement de systèmes, ``model checking'' probabiliste |
| Type du Projet: | |||
| Projet de recherche | Projet de recherche | Projet de recherche | Autre |
| multi-thématiques | avec infrastructure | ||
| XXX | |||
| Durée du projet: 3 ans |
| Description courte du Projet : (une demi-page maximum) |
| L'etude de la fiabilité de systèmes ou de la performabilité (évaluation de performances en présence de fautes réduisant les capacités de service) se heurte tout comme l'évaluation de performances à l'explosion combinatoire de l'espace des états mais aussi à l'évaluation de probabilités d'événements très faibles. L'analyse exhaustive est donc impossible et la simulation standard peu fiable. Le model checking probabiliste reposant sur des calculs de probabilites stationnaires ou transitoires ne dispose donc pas d'outils algorithmiques aussi performants que dans le cadre déterministe. Nos équipes ont proposé de nouvelles techniques qui ont su faire leur preuve dans un contexte assez semblable lié à l'explosion combinatoire des états, le calcul numeriques de probabilités très faibles et l'obtension de garantie : la décomposition modulaire et la représentation tensorielle compacte de l'espace des états et des transitions, les couplages de trajectoires pour déterminer des systèmes plus simples et fournissant une borne ou une garantie, les algorithmes de calcul de bornes, la convergence rapides des méthodes de Monte-Carlo, la simulation parfaite par couplage dans le passé garantissant une mesure exacte, l'emploi d'algorithmes adaptés à ces représentations tensorielles et aux ressources de type GRID, le lien avec des langages ou des formalismes de spécifications ou le model checking probabiliste. Le projet permettra d'étendre ces methodes et prototypes aux problématiques de la sûreté de fonctionnement tant d'un point de vue qualitatif que quantitatif. En effet pour un nombre grandissant d'applications (temps-réel ou embarquées, multimedia), la preuve formelle de correction ou d'absence de fautes ne peut être dissociée de l'évaluation quantitative du système. |
| Coordinateur du projet : | ||
| Nom | Prénom | Laboratoire (sigle éventuel et nom complet) |
| Plateau | Brigitte | ID, Informatique et Distribution |