وارسی ویژگی دسترس‌پذیری در سامانه‌های نرم‌افزاری پیچیده و هم‌روند با استفاده از الگوریتم‌های جستجوی هوشمند

روش وارسی مدل، روشی رسمی و موثر جهت تایید سامانه‌های نرم‌افزاری است که با تولید و بررسی همه حالت هایِ ممکنِ مدلی از سامانه نرم‌افزار به تحلیل آن می ‌پردازد. در سامانه‌های ایمنی - بحرانی، نمی توان ریسک بروز خطا را حتی در فرآیند تست پذیرفت و لذا لازم است فرآیند درستی‌یابی، قبل از پیاده‌ سازی و در سطح مدل انجام شود. استفاده از این روش به‌منظور بررسی خواصی مانند ایمنی ایجاب می‌ کند که تمام حالت‌ های قابل دسترس (تمام فضای حالت) تولید و سپس فضای حالت سامانه مورد نظر به‌صورت دقیق بررسی شوند. چالش اساسی روش وارسی مدل در سامانه‌های بزرگ و پیچیده که دارای فضای حالت گسترده و نامحدود هستند، مشکل انفجار فضای حالت (کمبود حافظه در تولید همه حالت‌های ممکن) است. سامانه‌های تبدیل گراف، از پرکاربردترین سامانه‌های مدل‌سازی رسمی و راه‌کاری مناسب به‌منظور مدل‌ سازی و وارسی سامانه‌های پیچیده هستند. در سامانه‌هایی که تایید ویژگی ایمنی غیرممکن است، می ‌توان با جستجویِ یک حالت قابل دسترسی که در آن پیکربندی خاصی (به‌عنوان مثال خطا یا رفتار نامطلوب) رخ می ‌دهد، ویژگی ایمنی را رد کرد. مطالعات اخیر حاکی از آن است که اکتشاف جزئی و هوشمندانه بخشی از فضای حالت می‌ تواند راه حل مناسبی برای مشکل انفجار فضای حالت باشد. هدف این پژوهش، استفاده از الگوریتم جنگل تصادفی در وارسی مدل است که می‌تواند با گزینش تعداد محدودی مسیر امیدبخش مشکل انفجار فضای حالت را برطرف سازد. مسیری امیدبخش است که احتمال رسیدن به یک جواب از طریق این مسیر، بیشتر از بقیه مسیرها باشد. در روش پیشنهادی، ابتدا مدل کوچکی از سامانه با استفاده از زبان رسمی سامانه توصیف گراف (gts) ایجاد، سپس، از فضای حالت مدل کوچک، مجموعه‌ آموزشی از مسیرهایی که به هدف می‌رسند ایجاد می‌شود. پس‌ازآن، مجموعه آموزشی تولیدشده در اختیار الگوریتم جنگل تصادفی قرار داده می‌شود تا روابط منطقی موجود در آن شناسایی و کشف شوند. در مرحله بعد از دانش به‌دست‌آمده جهت پیمایش هوشمند و غیر کامل فضایِ حالتِ مدلِ بزرگ استفاده می‌شود. رویکرد پیشنهادی برای تایید ویژگی دسترس‌پذیری و رد ویژگی ایمنی در سامانه‌های بزرگ و پیچیده که ایجاد تمام فضای حالت سامانه ناممکن است، استفاده می‌ شود. به منظور ارزیابی رویکرد پیشنهادی، این رویکرد در ابزار grooveکه از ابزار متن‌باز برای طراحی و وارسی مدل برای سامانه‌های تبدیل گراف است، اجراشده است. نتایج نشان می‌دهند که روش پیشنهادی ازنظر میانگین زمان اجرا و طول شاهد تولیدشده نسبت به روش‌های مورد مقایسه عملکرد بهتری دارد.

Reachability checking in complex and concurrent software systems using intelligent search methods

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 safetycritical 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.