{"id":7999,"date":"2019-05-02T10:48:51","date_gmt":"2019-05-02T09:48:51","guid":{"rendered":"http:\/\/synthese.univ-annaba.dz\/?p=7999"},"modified":"2019-05-06T12:44:25","modified_gmt":"2019-05-06T11:44:25","slug":"a-process-oriented-verification-and-validation-for-real-time-embedded-systems","status":"publish","type":"post","link":"https:\/\/synthese.univ-annaba.dz\/?p=7999","title":{"rendered":"A Process &#8211; oriented verification and validation for real time embedded systems"},"content":{"rendered":"<div><strong>Num\u00e9ro de la revue<\/strong>: Volume 25 , Num\u00e9ro 1<br \/>\n<strong>Auteurs<\/strong>: Nadia Chabbat &amp; Salim Ghanemi<\/div>\n<div><\/div>\n<div>\u00a0Department of Computer Sciences, Badji Mokhtar Annaba University, Po Box 12, Annaba, 23000, Algeria.<\/div>\n<div>\n<p style=\"text-align: right;\"><a href=\"http:\/\/synthese.univ-annaba.dz\/wp-content\/uploads\/2019\/05\/6-41.17-1.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<\/div>\n<p style=\"text-align: justify;\"><strong>ABSTRACT <\/strong><\/p>\n<p style=\"text-align: justify;\">Based on formal and robust concepts, the real-time embedded systems allow meeting the requirements for the quality of the systems. Considering the UML MARTE profile as the standard by excellence, it has been the most used in the modelling and analysis of systems. In addition, for the support of time constraints, the CCSL language (Clock Constraint Specification Language) has been proposed. However, the MARTE-CCSL profile allows only formal verification, which represents only the static validation. As a complement to the analysis, it is essential to consider the dynamic validation step as well. In this paper, we suggest a hybrid process-oriented verification approach (HV&amp;V) for MARTE-CCSL models. The HV&amp;V approach is based on a transformation of MARTE-CCSL models to Timed CSP (Communicating Sequential Processes) models. Thus, the Timed CSP model and the generated counter-examples will be automatically used by the validation step. This last step helps to quickly generate a prototype that is functional and verifiable at low cost. The approach is tested on the elevator control system.<\/p>\n<p style=\"text-align: justify;\"><strong>Key words<\/strong><\/p>\n<p style=\"text-align: justify;\">Real Time Embedded Systems\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 (RTES), Timed CSP (Communicating Sequential Processes), Clock Constraint Specification Language (CCSL), MARTE (Modeling and Analysis of Real Time Embedded Systems), V&amp;V (Verification &amp; Validation)<\/p>\n<p>&nbsp;<\/p>\n<p>&nbsp;<\/p>\n<p>&nbsp;<\/p>\n<p>&nbsp;<\/p>\n<p>&nbsp;<\/p>\n<p>&nbsp;<\/p>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Num\u00e9ro de la revue: Volume 25 , Num\u00e9ro 1 Auteurs: Nadia Chabbat &amp; Salim Ghanemi \u00a0Department of Computer Sciences, Badji Mokhtar Annaba University, Po Box 12, Annaba, 23000, Algeria. T\u00e9l\u00e9charger l&rsquo;article ABSTRACT Based on formal and robust concepts, the real-time &hellip; <a href=\"https:\/\/synthese.univ-annaba.dz\/?p=7999\">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":[1352],"tags":[],"class_list":["post-7999","post","type-post","status-publish","format-standard","hentry","category-synthese-251"],"_links":{"self":[{"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=\/wp\/v2\/posts\/7999","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=7999"}],"version-history":[{"count":3,"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=\/wp\/v2\/posts\/7999\/revisions"}],"predecessor-version":[{"id":8093,"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=\/wp\/v2\/posts\/7999\/revisions\/8093"}],"wp:attachment":[{"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=7999"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=7999"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/synthese.univ-annaba.dz\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=7999"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}