HMM_model-checker pour la vérification probabiliste
Other Title(s)
HMM_model-checker for probabilistic verification
Joint Authors
Source
Issue
Vol. 2017, Issue 35 (31 Dec. 2017), pp.14-24, 11 p.
Publisher
Annaba Badji Mokhtar University
Publication Date
2017-12-31
Country of Publication
Algeria
No. of Pages
11
Main Subjects
Information Technology and Computer Science
Abstract EN
Probabilistic verification for embedded systems continues to attract more and more followers in the research community.
Given a probabilistic model, a formula of temporal logic, describing a property of a system and an exploration algorithm to check whether the property is satisfied or not, the purpose is to achieve a safe system.
This work presents some innovative aspects such as the Hidden Markov Model (HMM) as a new model, an implementation of the algorithm for POCTL to allow properties verification on the HMM model, a design and implementation in the Netbeans environment of a probabilistic model-checker called "HMM_Model-Checker", and to raise the level of model abstraction, we have integrated the JaHMM library which allows to create an HMM from the parameters introduced by the user.
A real case study of embedded system: the Hubble Space Telescope, followed in order to consolidate our words.
Abstract FRE
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.
American Psychological Association (APA)
Ferroum, Assia& Boudour, Rashid. 2017. HMM_model-checker pour la vérification probabiliste. Synthèse،Vol. 2017, no. 35, pp.14-24.
https://search.emarefa.net/detail/BIM-811063
Modern Language Association (MLA)
Ferroum, Assia& Boudour, Rashid. HMM_model-checker pour la vérification probabiliste. Synthèse No. 35 (2017), pp.14-24.
https://search.emarefa.net/detail/BIM-811063
American Medical Association (AMA)
Ferroum, Assia& Boudour, Rashid. HMM_model-checker pour la vérification probabiliste. Synthèse. 2017. Vol. 2017, no. 35, pp.14-24.
https://search.emarefa.net/detail/BIM-811063
Data Type
Journal Articles
Language
French
Notes
Includes bibliographical references : p. 24
Record ID
BIM-811063
