Méthodes formelles. Intégration des méthodes formelles dans le processus de développement de systèmes temps réel. Systèmes de transitions (TS). Extensions des TS aux données, au temps et aux probabilités. Automates étendus. Automates temporisés. Automates probabilistes. Abstractions/comparaisons des TS. Modélisation des programmes séquentiels/concurrents, circuits électriques, etc.  Logiques temporelles linéaires. Logiques temporelles de branchement. Model-checking explicite. Model-checking des automates temporisés. Model-checking symbolique basé sur les diagrammes binaires de décision. Model-checking borné basé sur la satisfiabilité (SAT/SMT). Software model-checking. Model-checking probabiliste. Résolution de problèmes divers par model-checking. Synthèse de contrôleurs. Contrôle et analyse formelle de l'ordonnançabilité de tâches temps réel.  Décidabilité et complexité de vérification.