Conception et réalisation d'nn model-checher probabiliste à base de hmm application aux systèmes embarqués

Voir Plus Voir Moins

Afficher le Résumé

Au jour d’aujourd’hui, la vérification probabiliste pour systèmes embarqués continue à susciter de plus en plus d’adeptes dans la communauté de chercheurs. Etant donnée une formule de la logique POCTL, décrivant les spécifications d'un système, un modèle HMM, et un algorithme d’exploration permettant de vérifier si cette dernière est satisfaite ou non. Ce travail présente quelques aspects novateurs dans le domaine : le HMM comme nouveau modèle, une adaptation de l’algorithme de model-checking pour PCTL à POCTL pour permettre la vérification des propriétés sur le modèle HMM, une implémentation dans l’environnement Netbeans 6.5 d’un outil baptisé « HMM_Model-Checker ». Une étude de cas d’un système embarqué réel HST, a suivi pour consolider nos propos.