| Dans ce mémoire, nous présentons l'évaluation de modèle, appelée en anglais «model-checking », pour les processus de Markov étiquetés. Ces derniers sont des systèmes de transitions probabilistes dont l'ensemble des états est non-dénombrable. Ils servent à modéliser des systèmes qui ont un comportement aléatoire ou à approximer des systèmes complexes. Les contributions que nous apportons à ce domaine sont la définition d'un langage formel pour décrire une famille de systèmes probabilistes continus, la formalisation d'algorithmes pour la vérification formelle ainsi qu'une implémentation en Java d'un outil pouvant vérifier si un système vérifie une formule d'une logique probabiliste. Nous présentons aussi dans le document une étude de cas ainsi que des résultats obtenus avec l'implémentation. |
