Cette thèse traite des méthodes formelles pour les automates temporisés, de leurs actions sur la réalité, et des informations que l’on peut apprendre grâce à ces observations. Elle propose différentes contributions dans trois domaines distincts : la théorie des jeux et la génération de tests, vue comme un moyen de contrôler un système à l’aide de méthodes formelles ; l’estimation d’état, qui déduit les configurations possibles d’un système à partir d’observations au moyen d’une construction formelle ; l’apprentissage actif de modèles, qui propose de construire un modèle d’un système en lui demandant des observations, en les orientant selon les besoins de la tâche. Aussi diverses qu’elles puissent paraître, ces contributions sont liées par le formalisme sous-jacent, les abstractions utilisées et les préoccupations qui caractérisent les interactions entre les modèles formels et la réalité. De plus, elles bénéficient les unes des autres dans la pratique, formant un cercle vertueux : la capacité d’apprendre de la réalité permet de meilleurs modèles, qui à leur tour permettent un contrôle plus fin des systèmes, ce qui favorise les processus d’apprentissage. Nous relions ces différentes contributions entre elles sur la base de ces motifs, et nous plaidons pour un rapprochement entre les méthodes et les communautés d’apprentissage de modèles et de méthodes formelles.