Signal and Data Processing

fa وارسی ویژگی دسترس‌پذیری در سامانه‌های نرم‌افزاری پیچیده و هم‌روند با استفاده از الگوریتم‌های جستجوی هوشمند Reachability checking in complex and concurrent software systems using intelligent search methods مقالات پردازش داده‌های رقمی Paper پژوهشي Research <div style="text-align: justify;">روش وارسی مدل، روشی رسمی و مؤثر جهت تأیید سامانه‌های نرم‌افزاری است که با تولید و بررسی همه حالتهایِ ممکنِ مدلی از سامانه نرم‌افزار به تحلیل آن می‌پردازد. در سامانه‌های ایمنی– بحرانی، نمیتوان ریسک بروز خطا را حتی در فرآیند تست پذیرفت و لذا لازم است فرآیند درستی‌یابی، قبل از پیاده‌سازی و در سطح مدل انجام شود. استفاده از این روش به‌منظور بررسی خواصی مانند ایمنی ایجاب می‌کند که تمام حالت‌های قابل دسترس (تمام فضای حالت) تولید و سپس فضای حالت سامانه مورد نظر به‌صورت دقیق بررسی شوند. چالش اساسی روش وارسی مدل در سامانه‌های بزرگ و پیچیده که دارای فضای حالت گسترده و نامحدود هستند، مشکل انفجار فضای حالت (کمبود حافظه در تولید همه حالت‌های ممکن) است. سامانه‌های تبدیل گراف، از پرکاربردترین سامانه‌های مدل‌سازی رسمی و راه‌کاری مناسب به‌منظور مدل‌سازی و وارسی سامانه‌های پیچیده هستند. در سامانه‌هایی که تأیید ویژگی ایمنی غیرممکن است، می‌توان با جستجویِ یک حالت قابل دسترسی که در آن پیکربندی خاصی (به‌عنوان مثال خطا یا رفتار نامطلوب) رخ می‌دهد، ویژگی ایمنی را رد کرد. مطالعات اخیر حاکی از آن است که اکتشاف جزئی و هوشمندانه بخشی از فضای حالت می‌تواند راه حل مناسبی برای مشکل انفجار فضای حالت باشد. هدف این پژوهش، استفاده از الگوریتم جنگل تصادفی در وارسی مدل است که می‌تواند با گزینش تعداد محدودی مسیر امیدبخش مشکل انفجار فضای حالت را برطرف سازد. مسیری امیدبخش است که احتمال رسیدن به یک جواب از طریق این مسیر، بیشتر از بقیه مسیرها باشد. در روش پیشنهادی، ابتدا مدل کوچکی از سامانه با استفاده از زبان رسمی سامانه توصیف گراف (GTS) ایجاد، سپس، از فضای حالت مدل کوچک، مجموعه‌ آموزشی از مسیرهایی که به هدف می‌رسند ایجاد می‌شود. پس‌ازآن، مجموعه آموزشی تولیدشده در اختیار الگوریتم جنگل تصادفی قرار داده می‌شود تا روابط منطقی موجود در آن شناسایی و کشف شوند. در مرحله بعد از دانش به‌دست‌آمده جهت پیمایش هوشمند و غیر کامل فضایِ حالتِ مدلِ بزرگ استفاده می‌شود. رویکرد پیشنهادی برای تأیید ویژگی دسترس‌پذیری و رد ویژگی ایمنی در سامانه‌های بزرگ و پیچیده که ایجاد تمام فضای حالت سامانه ناممکن است، استفاده می‌شود. به منظور ارزیابی رویکرد پیشنهادی، این رویکرد  در ابزار GROOVEکه از ابزار متن‌باز برای طراحی و وارسی مدل برای سامانه‌های تبدیل گراف است، اجراشده است. نتایج نشان می‌دهند که روش پیشنهادی ازنظر میانگین زمان اجرا و طول شاهد تولیدشده نسبت به روش‌های مورد مقایسه عملکرد بهتری دارد.</div> <div style="text-align: justify;">The model checking technique is a formal and effective method for verifying software systems, which analyses it via generating and examining all possible states of a model of the software system. In safety-critical systems, one could not admit the risk of error even in the testing process, therefore it is necessary to carry out the verification process before implementation and at the model level. Using this technique to evaluate properties such as security entails all available states (all state space) being generated, then the state space of the system in question be carefully examined. The main challenge of the model checking technique in large and complex systems with wide or infinite state space is the problem of state space explosion (lack of memory in the generation of all possible states). Graph transformation systems are one of the most widely used formal modeling systems and a suitable solution for modeling and checking complex systems. In systems where security property verification is not possible, the security feature can be refuted by searching for an accessible mode in which a specific configuration (e.g. error or undesirable behavior) occurs. Recent studies advocate that partial and intelligent exploration of part of the state space could be a good solution to the problem of state space explosion. The goal of this study is to use the random forest algorithm in the model checking which can solve the problem of state space explosion by selecting a few promising paths. A path is hopeful whenever the probability of reaching an answer through this path is higher than other paths. In the proposed method, a small model of the system is first created using the official language of the Graph Description System (GTS). Afterwards, a training data set of paths to the goal is generated from the small model mode space. The generated training data set is then provided to the random forest algorithm to identify and discover the logical relationships within it. In the next stage, the acquired knowledge is used to intelligently explore the incomplete space of the large model state. The proposed approach is used in the verification of the reachability property and to refute the safety feature in large and complex systems where it is impossible to generate the entire system state space. In order to evaluate the proposed approach, it has been implemented in GROOVE which is an open source tool for designing and checking models in graph conversion systems. The results indicate that the proposed method performs better than the compared methods in terms of average running time and the length of the generated witness.</div> وارسی مدل, تأیید سامانه‌های نرم‌افزاری, کشف دانش, انفجار فضای حالت, جستجوی هوشمند Software systems verification, Knowledge discovery, State space explosion, intelligent search 153 166 http://jsdp.rcisp.ac.ir/browse.php?a_code=A-10-1924-1&slc_lang=fa&sid=1 jaafar partabian جعفر پرتابیان Jaafar_partabian@yahoo.com 100319475328460011414 100319475328460011414 No azad university دانشگاه آزاد اسلامی، واحد یاسوج vahid rafe وحید رافع v-rafe@araku.ac.ir 100319475328460011415 100319475328460011415 Yes arak university دانشگاه اراک hamid parvin حمید پروین parvinhamid@gmail.com 100319475328460011416 100319475328460011416 No azad university دانشگاه آزاد اسلامی، واحد نورآباد ممسنی samad nejatian صمد نجاتیان samad.nej.2007@gmail.com 100319475328460011417 100319475328460011417 No azad university دانشگاه آزاد اسلامی، واحد یاسوج Karamollah bagherifard کرم‌اله باقری‌فرد k.bagheri@iauyasooj.ac.ir 100319475328460011418 100319475328460011418 No Yasooj Branch, Islamic Azad University دانشگاه آزاد اسلامی، واحد یاسوج