{"id":6046,"date":"2016-10-31T09:53:58","date_gmt":"2016-10-31T08:53:58","guid":{"rendered":"http:\/\/dpubma.univ-annaba.dz\/?p=6046"},"modified":"2016-10-31T14:00:18","modified_gmt":"2016-10-31T13:00:18","slug":"un-verificateur-symbolique-efficace","status":"publish","type":"post","link":"https:\/\/synthese.univ-annaba.dz\/?p=6046","title":{"rendered":"Un v\u00e9rificateur symbolique efficace"},"content":{"rendered":"<p style=\"text-align: justify;\" align=\"center\"><strong>Num\u00e9ro de la revue<\/strong>:\u00a033<br \/>\n<strong>Auteurs<\/strong>: Ahlem Ferdenache\u00a0&amp; Rachid Boudour<\/p>\n<p><em>Laboratoire de syst\u00e8mes embarqu\u00e9s \u2013LASE, Universit\u00e9 Badji Mokhtar- BP 12, Annaba 23000, Alg\u00e9rie.<\/em><br \/>\n<a href=\"#_ftnref1\" name=\"_ftn1\"><\/a><\/p>\n<p>&nbsp;<\/p>\n<p style=\"text-align: right;\"><a href=\"http:\/\/dpubma.univ-annaba.dz\/wp-content\/uploads\/2016\/10\/9-43-15.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;\">En g\u00e9nie informatique d\u2019aujourd\u2019hui, l\u2019objectif est d\u2019arriver \u00e0 des m\u00e9thodes et des outils qui peuvent ex\u00e9cuter la v\u00e9rification de mod\u00e8le automatiquement : le model checking. Le probl\u00e8me du model checking est le grand espace d\u2019\u00e9tats. Une des solutions est d\u2019utiliser le model checking symbolique combin\u00e9e \u00e0 des structures de donn\u00e9es compactes.\u00a0 Le but de ce papier est de concevoir et mettre en application un nouvel outil performant, pour v\u00e9rifier des propri\u00e9t\u00e9s importantes dans les syst\u00e8mes critiques bas\u00e9s sur la notion d\u2019\u00e9tat symbolique ainsi que des structures de donn\u00e9es DBM (Difference Bound Matrices). Les sp\u00e9cifications sont exprim\u00e9es \u00e0 l\u2019aide d\u2019automates temporis\u00e9s pour le syst\u00e8me et de logique temps r\u00e9el pour les propri\u00e9t\u00e9s. Les r\u00e9sultats obtenus sont compar\u00e9s \u00e0 ceux de la litt\u00e9rature.<\/p>\n<p style=\"text-align: justify;\"><strong>Mots cl\u00e9s :<\/strong><em>v\u00e9rification symbolique &#8211; automates temporis\u00e9s &#8211; TCTL\u2013\u00e0 la vol\u00e9e &#8211; DBM.<\/em><\/p>\n<p style=\"text-align: justify;\">\n","protected":false},"excerpt":{"rendered":"<p>Num\u00e9ro de la revue:\u00a033 Auteurs: Ahlem Ferdenache\u00a0&amp; 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 En g\u00e9nie informatique d\u2019aujourd\u2019hui, l\u2019objectif est d\u2019arriver \u00e0 des m\u00e9thodes et des outils qui &hellip; <a href=\"https:\/\/synthese.univ-annaba.dz\/?p=6046\">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,1078],"tags":[1114,1112,1113,1111],"class_list":["post-6046","post","type-post","status-publish","format-standard","hentry","category-synthese-2","category-synthese-n-33","tag-a-la-volee-dbm","tag-automates-temporises","tag-tctl","tag-verification-symbolique"],"_links":{"self":[{"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=\/wp\/v2\/posts\/6046","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=6046"}],"version-history":[{"count":2,"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=\/wp\/v2\/posts\/6046\/revisions"}],"predecessor-version":[{"id":6115,"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=\/wp\/v2\/posts\/6046\/revisions\/6115"}],"wp:attachment":[{"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=6046"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=6046"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=6046"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}