{"id":7052,"date":"2017-11-26T14:24:35","date_gmt":"2017-11-26T13:24:35","guid":{"rendered":"http:\/\/dpubma.univ-annaba.dz\/?p=7052"},"modified":"2017-11-26T14:25:29","modified_gmt":"2017-11-26T13:25:29","slug":"hmm_model-checker-pour-la-verification-probabiliste","status":"publish","type":"post","link":"https:\/\/synthese.univ-annaba.dz\/?p=7052","title":{"rendered":"HMM_Model-Checker pour la v\u00e9rification probabiliste"},"content":{"rendered":"<p style=\"text-align: justify;\" align=\"center\"><strong>Num\u00e9ro de la revue<\/strong>:\u00a035<br \/>\n<strong>Auteurs<\/strong>: Assia Ferroum\u00a0\u00a0&amp;\u00a0 Rachid Boudour<\/p>\n<p><em>Laboratoire de syst\u00e8mes embarqu\u00e9s \u2013LASE-, Universit\u00e9 Badji Mokhtar.<\/em><\/p>\n<p><em>BP 12, Annaba, 23000, Alg\u00e9rie.<\/em><\/p>\n<p>&nbsp;<\/p>\n<p style=\"text-align: right;\"><a href=\"http:\/\/dpubma.univ-annaba.dz\/wp-content\/uploads\/2017\/11\/2-69.16.pdf\"><strong>T\u00e9l\u00e9charger l&rsquo;article<img loading=\"lazy\" decoding=\"async\" class=\" wp-image-709 alignright\" style=\"margin-top: -10px; margin-bottom: -10px;\" src=\"\/wp-content\/uploads\/2014\/04\/p2.jpg\" alt=\"p2\" width=\"37\" height=\"35\" srcset=\"https:\/\/synthese.univ-annaba.dz\/wp-content\/uploads\/2014\/04\/p2.jpg 113w, https:\/\/synthese.univ-annaba.dz\/wp-content\/uploads\/2014\/04\/p2-24x24.jpg 24w, https:\/\/synthese.univ-annaba.dz\/wp-content\/uploads\/2014\/04\/p2-48x46.jpg 48w\" sizes=\"auto, (max-width: 37px) 100vw, 37px\" \/><\/strong><\/a><\/p>\n<p style=\"text-align: justify;\"><strong>R\u00e9sum\u00e9<\/strong><\/p>\n<p style=\"text-align: justify;\">La v\u00e9rification probabiliste des\u00a0 syst\u00e8mes embarqu\u00e9s continue de compter de plus en plus d\u2019adeptes dans la communaut\u00e9 de chercheurs. \u00c9tant donn\u00e9 un mod\u00e8le probabiliste, une formule de la logique temporelle, d\u00e9crivant une propri\u00e9t\u00e9 du syst\u00e8me et un algorithme d\u2019exploration permettant de v\u00e9rifier si cette derni\u00e8re est satisfaite ou non, la finalit\u00e9 est d\u2019arriver \u00e0 un syst\u00e8me fiable. Ce travail\u00a0 pr\u00e9sente quelques aspects novateurs dans le domaine: le mod\u00e8le de Markov cach\u00e9 (HMM) comme nouveau\u00a0 mod\u00e8le en v\u00e9rification probabiliste, une impl\u00e9mentation d\u2019un algorithme pour POCTL afin de permettre la v\u00e9rification des propri\u00e9t\u00e9s sur le mod\u00e8le HMM, une conception et une impl\u00e9mentation dans l\u2019environnement Netbeans d\u2019un v\u00e9rificateur probabiliste baptis\u00e9 \u00abHMM_Model-Checker\u00bb, et pour \u00e9lever le niveau d\u2019abstraction du mod\u00e8le, nous avons int\u00e9gr\u00e9 la biblioth\u00e8que JaHMM qui permet de cr\u00e9er un HMM \u00e0 partir de param\u00e8tres introduits par l\u2019utilisateur, Une \u00e9tude de cas d\u2019un syst\u00e8me embarqu\u00e9 r\u00e9el: le t\u00e9lescope spatial Hubble, a suivi pour consolider nos propos.<\/p>\n<p style=\"text-align: justify;\"><strong>Mots cl\u00e9s\u00a0: <\/strong>V\u00e9rification de mod\u00e8le probabiliste\u2013Syst\u00e8mes embarqu\u00e9s\u2013Mod\u00e8le de Markov cach\u00e9\u2013Logique\u00a0 probabiliste \u2013T\u00e9lescope Hubble.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Num\u00e9ro de la revue:\u00a035 Auteurs: Assia Ferroum\u00a0\u00a0&amp;\u00a0 Rachid Boudour Laboratoire de syst\u00e8mes embarqu\u00e9s \u2013LASE-, Universit\u00e9 Badji Mokhtar. BP 12, Annaba, 23000, Alg\u00e9rie. &nbsp; T\u00e9l\u00e9charger l&rsquo;article R\u00e9sum\u00e9 La v\u00e9rification probabiliste des\u00a0 syst\u00e8mes embarqu\u00e9s continue de compter de plus en plus d\u2019adeptes &hellip; <a href=\"https:\/\/synthese.univ-annaba.dz\/?p=7052\">Lire la suite <span class=\"meta-nav\">&raquo;<\/span><\/a><\/p>\n","protected":false},"author":5,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[16,1219],"tags":[1221],"class_list":["post-7052","post","type-post","status-publish","format-standard","hentry","category-synthese-2","category-synthese-n-35","tag-verification-de-modele-probabiliste-systemes-embarques-modele-de-markov-cache-logique-probabiliste-telescope-hubble"],"_links":{"self":[{"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=\/wp\/v2\/posts\/7052","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=\/wp\/v2\/users\/5"}],"replies":[{"embeddable":true,"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=7052"}],"version-history":[{"count":3,"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=\/wp\/v2\/posts\/7052\/revisions"}],"predecessor-version":[{"id":7057,"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=\/wp\/v2\/posts\/7052\/revisions\/7057"}],"wp:attachment":[{"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=7052"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=7052"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=7052"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}