Model Checking Statistique pour les Systemes Larges

Nous proposons dans cette thse une nouvelle mthode de vrification des proprits stationnaires dans les systmes ` large chelle et nous appliquons cette mthode sur la vrification des proprits de dependabilit dans les systmes informatiques `a large chelle. Nous proposons d'utiliser la simulation parfaite et les mthodes statistiques pour effectuer le model checking probabiliste, afin de vrifier les proprits stationnaires des systmes informatiques large chelle et analyser ainsi leur suret de fonctionnement. La simulation parfaite avec le couplage dans le pass est reconnue efficace et prcise pour calculer la distribution stationnaire. Nous proposons dans cette thse de nouveaux algorithmes de model checking qui reposent sur les mthodes statistiques et sur la simulation parfaite. On applique cette mthode de model checking sur tudes de cas issues de quelques " benchmarks " connues. Nous tudions l'efficacit e et le passage l'chelle de nos algorithmes propos es. Nous comparons ainsi la performance des diffrentes mthodes statistiques existantes en les intgrant dans notre mthode de vrification.