Les logiciels sont devenus une partie importante de notre vie quotidienne, car ils sont maintenant utilisés dans de nombreux périphériques hétérogènes, tels que nos téléphones, nos voitures, nos appareils ménagers, etc. Ces périphériques sont parsemés d’un certain nombre de logiciels intégrés, chacun gérant une tâche spécifique. Ces logiciels intégrés sont conçus pour fonctionner à l’intérieur de systèmes plus vastes avec un matériel varié et hétérogène et des ressources limitées. L'utilisation de logiciels embarqués est motivée par la flexibilité et la simplicité que ces logiciels peuvent garantir, ainsi que par la réduction des coûts. Les Cyber-Physical System (CPS) sont des logiciels utilisés pour contrôler des systèmes physiques. Les CPS sont souvent intégrés et s'exécutent en temps réel, ce qui signifie qu'ils doivent réagir aux événements externes. Un CPS complexe peut contenir de nombreux systèmes en temps réel. Le fait que ces systèmes puissent être utilisés dans des domaines critiques tels que la médecine ou les transports exige un haut niveau de sécurité pour ces systèmes. Les systèmes temps réel (RTS), par définition, sont des systèmes informatiques de traitement qui doivent répondre à des entrées générées de manière externe. Ils sont appelés temps réel car leur réponse doit respecter des contraintes de temps strictes. Par conséquent, l'exactitude de ces systèmes ne dépend pas seulement de l'exactitude des résultats de leur traitement, mais également du moment auquel ces résultats sont donnés. Le principal problème lié à l'utilisation de systèmes temps réel est la difficulté de vérifier leurs contraintes de synchronisation. Un moyen de vérifier les contraintes de temps peut consister à utiliser la théorie de la planification, stratégie utilisée pour partager les ressources système entre ses différents composants. Outre les contraintes de temps, il convient de prendre en compte d'autres contraintes, telles que la consommation d'énergie ou la sécurité. Plusieurs méthodes de vérification ont été utilisées au cours des dernières années, mais avec la complexité croissante des logiciels embarqués, ces méthodes atteignent leurs limites. C'est pourquoi les chercheurs se concentrent maintenant sur la recherche de nouvelles méthodes et de nouveaux formalismes capables de vérifier l'exactitude des systèmes les plus complexes. Aujourd'hui, une classe de méthodes de vérification bien utilisées est les techniques basées sur des modèles. Ces techniques décrivent le comportement du système considéré à l'aide de formalismes mathématiques, puis, à l'aide de méthodes appropriées, permettent d'évaluer l'efficacité du système par rapport à un ensemble de propriétés. Dans ce manuscrit, nous nous concentrons sur l'utilisation de techniques basées sur des modèles pour développer de nouvelles techniques de planification afin d'analyser et de valider la satisfiabilité d'un certain nombre de propriétés sur des systèmes temps réel. L'idée principale est d'exploiter la théorie de l'ordonnancement pour proposer ces nouvelles techniques. Pour ce faire, nous proposons un certain nombre de nouveaux modèles afin de vérifier la satisfiabilité d'un certain nombre de propriétés telles que l'ordonnancement, la consommation d'énergie ou la fuite d'informations.