پردازش علائم و داده ها، جلد ۱۹، شماره ۱، صفحات ۰-۰
عنوان فارسی وارسی ویژگی دسترس‌پذیری در سیستم‌های نرم-افزاری پیچیده و همروند با استفاده از الگوریتم‌های جستجوی هوشمند
چکیده فارسی مقاله تکنیک وارسی مدل، روشی رسمی و موثر جهت تایید سیستم­های نرم­افزاری است. چالش اساسی تکنیک وارسی مدل در سیستم­های پیچیده و بزرگ که دارای فضای حالت گسترده و یا نامحدود می­باشند، مشکل انفجار فضای حالت است. در روش پیشنهادی، ابتدا مجموعه داده­ای از مسیرهای هدف و غیر هدف از فضای حالت مدل کوچک مساله ایجاد می­شود. مجموعه داده­ی برچسب­گذاری شده به الگوریتم یادگیر ماشین ترکیبی آموزش داده می­شود تا روابط منطقی موجود در مسیرها شناسایی و کشف شوند. سپس از دانش بدست آمده جهت پیمایش هوشمند و غیرکامل فضایِ حالتِ مدلِ بزرگ به منظور وارسی ویژگی دسترس پذیری استفاده می­شود. روش یادگیری ماشین استفاده شده در راه­حل پیشنهادی، ترکیبی از درخت­های تصمیم است که از نمونه­گیری با جایگزینی استفاده می­کند. این روش یادگیری، T درخت تصمیم ایجاد کرده و در نهایت با مکانیسم رای اکثریت، برچسب نهایی مسیرهای موجود در فضای حالت مدل بزرگ را تعیین می­کند. رویکرد پیشنهادی در ابزار GROOVEکه از ابزار متن باز برای طراحی و بررسی مدل سیستم­های تبدیل گراف است، اجرا شده است.    
کلیدواژه‌های فارسی مقاله وارسی مدل، انفجار فضای حالت، ویژگی دسترس پذیری، یادگیری ماشین، جستجوی هوشمند
عنوان انگلیسی Reachability checking in complex and concurrent software systems using intelligent search methods
چکیده انگلیسی مقاله Software system verification is an efficient technique for ensuring the correctness of a software product, especially in safety-critical systems in which a small bug may have disastrous consequences. The goal of software verification is to ensure that the product fulfills the requirements. Studies show that the cost of finding and fixing errors in design time is less than finding and fixing them after implementation. One of the most efficient formal verification techniques is model checking. Model checking is an automated approach to verify different properties on formal models and before implementation. In model checking techniques, a model should be designed along with the essential properties of the system to be checked. These properties are usually specified through temporal logic. Both the formal model and the properties are fed into a model checker as its input. Then, the model checker generates all reachable state (state space) automatically. By searching the state space, model checkers verify the property. One of the main problems of model checking techniques is that in complex systems, the state space is too large or even infinitely grows. This problem is called the state space explosion. State space explosion problem usually occurs due to computational resource limitations, and it prevents model checker from working correctly. In this paper, we propose an efficient approach to verify reachability properties in complex systems. The proposed method avoid state space explosion by partially and intelligently exploring state space. To do so, a small model of the system is generated, and the state space is explored entirely. Then, the reachability property is checked on the state space to find the goal state. After finding the goal states, all paths from the initial state leading to the goal state are labeled to distinguish between paths that are leading to the goal state and those who are not. The labeled paths are fed to the ensemble machine learning algorithm to detect logical relations among paths and also the existing knowledge in the state space. The acquired knowledge is used to partially and intelligently explore the state space of the main model for reachability analysis. This main model is larger and more complex than the smaller one. The machine learning algorithm used in the proposed solution is based on decision trees with sampling and replacement. In this learning method, after building T decision trees, T predictive models are also generated. Finally, using a voting mechanism, labels of paths in the state space of the main model is determined. This learning technique misbehaves in the cases in which at least half of the predictive models are wrong. This technique is better learned in comparison with the individual learning mechanisms. It also can detect more complicated relations in the state space. The proposed approach is implemented in GROOVE, which is an open-source toolset for designing and model checking of graph transformation systems. Our experiments show a better performance in terms of speed and memory usage in comparison with the other approaches. Our approach uses 42% less memory on average in comparison with the existing methods. It also generates 20% shorter witnesses, on average.
کلیدواژه‌های انگلیسی مقاله Model checking, State space explosion, Reachability property, intelligent search, machine learning
نویسندگان مقاله جعفر پرتابیان | jaafar partabian
azad university
دانشگاه آزاد

وحید رافع | vahid rafe
arak university
دانشگاه اراک

حمید پروین | hamid parvin
azad university
دانشگاه آزاد

صمد نجاتیان | samad nejatian
azad university
دانشگاه آزاد

نشانی اینترنتی http://jsdp.rcisp.ac.ir/browse.php?a_code=A-10-1924-1&slc_lang=fa&sid=1
فایل مقاله فایلی برای مقاله ذخیره نشده است
کد مقاله (doi)
زبان مقاله منتشر شده fa
موضوعات مقاله منتشر شده مقالات پردازش داده‌های رقمی
نوع مقاله منتشر شده پژوهشی
برگشت به: صفحه اول پایگاه   |   نسخه مرتبط   |   نشریه مرتبط   |   فهرست نشریات