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...