|
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 performances à l'explosion combinatoire de l'espace des états mais aussi à l'évaluation de probabilités d'événements très faibles. Du fait de la taille de l'espace d'états, il est en général impossible de tester de façon exhaustive l'ensemble des configurations d'un protocole ou d'un système partiellement redondant. L'évaluation de probabilité très faibles posent des problèmes numériques difficiles. Et les simulations non guidées ne convergent pas, faute d'échantilloner en un temps raisonnable les états ou transitions remarquables qui nous intéressent. 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. Toute la problématique de l'évaluation quantitative de la sécurité peut être résumé comme suit : un espace d'états trop grand où se produisent des événements trop rares. En évaluation de performances les équipes participant au projet ont développé de nouvelles techniques qui ont su faire leur preuve dans un contexte assez semblable lié à l'explosion combinatoire des états, le calcul numérique 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, les couplages de trajectoires pour déterminer des systèmes plus simples et fournissant une borne ou une garantie, 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 pour le logiciel. De même, de nombreux travaux dans la communauté ``Stochastic Process Algebra'' essaient de faire confluer les méthodes probabilites et celles du model checking probabilistes. En effet, pour un nombre grandissant d'applications (applications temps-reel ou embarquées, applications multimedia), la preuve formelle de correction ou d'absence de fautes ne peut être dissociée de l'évaluation quantitative du système. Le modèle général est celui des systèmes Markoviens car il est intrinsèquement associé à des algorithmes de calcul, ce qui n'est pas le cas des autres cadres probabilistes. Cependant, la modélisation par de très grandes chaînes de Markov soulève généralement deux problèmes, celui de l'obtension de la chaîne à partir des spécifications du problème, et celui des algorithmes de résolution numériques ou des simulations de la chaîne et des métriques associées à la fiabilité, disponibilité et sûreté d'un système, c'est à dire le calcul des distributions stationnaires ou transitoires, des délais avant absorbtion, des disponibilités cumulées, etc. Les équipes réunies ici ont apporté au cours des années passées des solutions à ces deux problèmes. |
