Synthèse
Volume 23, Numéro 2, Pages 14-24
2017-10-31
Hmm_model-checker Pour La Vérification Probabiliste
Auteurs : Ferroum Assia . Boudour Rachid .
Résumé
La vérification probabiliste des systèmes embarqués continue de compter de plus en plus d’adeptes dans la communauté de chercheurs. Étant donné un modèle probabiliste, une formule de la logique temporelle, décrivant une propriété du système et un algorithme d’exploration permettant de vérifier si cette dernière est satisfaite ou non, la finalité est d’arriver à un système fiable. Ce travail présente quelques aspects novateurs dans le domaine: le modèle de Markov caché (HMM) comme nouveau modèle en vérification probabiliste, une implémentation d’un algorithme pour POCTL afin de permettre la vérification des propriétés sur le modèle HMM, une conception et une implémentation dans l’environnement Netbeans d’un vérificateur probabiliste baptisé «HMM_Model-Checker», et pour élever le niveau d’abstraction du modèle, nous avons intégré la bibliothèque JaHMM qui permet de créer un HMM à partir de paramètres introduits par l’utilisateur, Une étude de cas d’un système embarqué réel: le télescope spatial Hubble, a suivi pour consolider nos propos.
Mots clés
Vérification de modèle probabiliste–Systèmes embarqués–Modèle de Markov caché–Logique probabiliste –Télescope Hubble.
Les articles similaires
تاوريريت حسام الدين
.
شاشه إيمان
.
ص 531-546.
Mechab Belaïd
.
Salem Mokadem
.
Mokhtari Mohamed.
.
Serier Boualem
.
Chama Mourad
.
pages 83-91.
Achouri Sihem
.
Redjel Bachir
.
pages 59-76.
Achouri S.
.
Redjel Bachir
.
Berdjan D.
.
pages 93-98.
Chachoua-harmim El Y.
.
Harmim A.
.
Mammeri A.
.
Yaïchi M.
.
pages 581-587.
