Mémoires de Fin d’Etudes
Etablissement
Université de Annaba - Badji Mokhtar
Affiliation
Département d’Informatique
Auteur
FERROUM, Assia
Directeur de thèse
Rachid BOUDOUR (Maitre de conférence)
Filière
Informatique
Diplôme
Magister
Titre
Conception et réalisation d’un model-checker probabiliste à base de HMM Application aux systèmes embarqués
Mots clés
Systèmes embarqués, Model- checking probabiliste, HMM, POCTL.
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. Étant 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.
Date de soutenance
2010.
Cote
004 FER.
Pagination
126 f.
Illusatration
fig.
Format
30 cm.
Statut
Soutenue