Projet  "Model Checking" stochastique pour la performabilité et la sûreté des systèmes informatiques

L’utilisation croissante des systèmes automatisés dans tous les aspects de nos vies donne une importance croissante à la sûreté de leur fonctionnement. La présence de tels systèmes dans des applications critiques, couplée à leur complexité croissante, rend indispensable leur vérification pour voir s’ils se comportent comme prévu. Ainsi le "model checking" qui est la mise en application des techniques formelles de vérification a un intérêt fondamental dans ce contexte. L’extension naturelle des techniques de vérification, qui sont devenues efficaces et répandues, était l’élargissement de modèles et de formalismes de spécifications auxquels le "model checking" peut être appliqué. De plus, puisque les comportements des systèmes réels sont stochastiques, le formalisme a été étendu au "model checking" probabiliste.

Différents formalismes dans lesquels le système considéré est défini par une chaîne de Markov ont été  proposés et la vérification des modèles markoviens peut être effectuée par analyse numérique ou par simulation. Dans le formalisme "model checking", les modèles considérés sont vérifiés pour décider si des contraintes sur les mesures étudiées sont satisfaites sans nécessairement connaître la valeur exacte de chaque mesure. De ce fait, il est possible d’appliquer les méthodes de bornes : on peut valider un modèle à partir des mesures bornantes, si la borne vérifie la contrainte imposée alors le modèle est vérifié, sinon on ne peut pas décider et il faut raffiner le modèle bornant pour améliorer la qualité de la borne. Nous proposons donc d’appliquer les méthodes de Comparaison Stochastique qui permettent de construire des bornes sur les distributions transitoires et la distribution stationnaire. Nous proposons également d’appliquer l’approche par simulation parfaite avec le couplage dans le passé dont l’efficacité a été démontrée pour calculer la distribution stationnaire lorsque le modèle est monotone. Nous envisagions d’élargir cette approche pour l’analyse transitoire et pour le "model checking" des modèles bornants à l'’aide de la monotonie stochastique. L’approche par bornes peut également apporter une solution dans le cadre du "model checking" infini qui est un problèmeme difficile à capturer.

De nombreux liens existent entre la vérification formelle utilisant le "model checking" et l’'évaluation quantitative de performance et de disponibilité. Notre grande expérience dans le cadre de l'’évaluation quantitative permettra sans aucun doutes d’obtenir des résultats intéressants dans le contexte du "model checking" stochastique

.