Ce livre propose des mod les multi-agents r actifs fond s sur un cadre formel pour la v rification de propri t s et leurs validations par la simulation et l'exp rimentation en consid rant la navigation multi-v hicules comme domaine d'application. La navigation multi-v hicules soul ve plusieurs probl matiques: navigation autonome, interaction v hicule-v hicule, ... Dans ce contexte, nous avons abord plus particuli rement les aspects suivants: la conduite en convoi (platooning lin aire) et la navigation autonome. Pour cela, nous utilisons le paradigme des syst mes multi-agents r actifs, en utilisant un mod le d'interactions inspir de la physique. Nous pla ons les syst mes multi-agents r actifs dans un cadre formel pour la v rification des propri t s, compte-tenu des contraintes de s curit impos es par la classe d'applications cible. Pour faire face la complexit des mod les, nous proposons une r gle et une m thode de v rification compositionnelle. Nous abordons galement la question de la validation du syst me multi-agents par la simulation et l'exp rimentation.