---

Aujourd´hui, de nombreux systèmes à base de composants sont critiques ; leur fonctionnement requiert un niveau de confiance maximal. Cette thèse propose un cadre de description haut niveau, où la vérification accompagne la modélisation du système, et limite le problème de l´explosion combinatoire du model checkingp par une vérification modulaire des composants du système. L´approche se base sur les observateurs, qui s´exécutent en parallèle d´un système sans en modifier le comportement global et permettent de décrire des propriétés. La modularité de la vérification vient de la possibilité de remplacer avec sûreté tout ou partie d´un système par un autre. Ceci est rendu possible par l´utilisation conjointe du model checking et de l´interprétation abstraite, ce qui assure le calcul d´un sur-ensemble des comportements du système. Alors que l´interprétation abstraite introduit des approximations, les observateurs permettent de distinguer des états qui auraient été fusionnés pour gagner la précision nécessaire. Ils pilotent les analyses en introduisant des instants d´observation. Décrits par l´utilisateur, ils permettent une mise au point interactive des états à fusionner.

---