L'étude 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 probabilités d'événements très faibles. L'analyse exhaustive est donc impossible et la simulation peu fiable. Le model checking probabiliste reposant sur des calculs de probabilités 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.