Dans ce papier, nous proposons une méthode d'évaluation de l'ordonnançabilité reposant sur une analyse markovienne. Tout d'abord, nous modélisons une application temps-réel en utilisant les chaînes de Markov. Nous intégrons ensuite la vérification des contraintes d'exécution. Pour diminuer la complexité, nous introduisons une technique de réduction compatible, d'une part avec l'application, et d'autre part avec les contraintes à vérifier.