این سایت در حال حاضر پشتیبانی نمی شود و امکان دارد داده های نشریات بروز نباشند
صفحه اصلی
درباره پایگاه
فهرست سامانه ها
الزامات سامانه ها
فهرست سازمانی
تماس با ما
JCR 2016
جستجوی مقالات
پنجشنبه 27 آذر 1404
رایانش نرم و فناوری اطلاعات
، جلد ۱۲، شماره ۱، صفحات ۴۱-۵۱
عنوان فارسی
وارسی ویژگی دسترس پذیری در سیستم های نرم افزاری پیچیده و همروند با رویکرد کشف دانش
چکیده فارسی مقاله
تکنیک وارسی مدل، روشی رسمی و مؤثر جهت تأیید سیستمهای نرمافزاری است که با تولید و بررسی همه حالتهای ممکنِ مدلی از سیستم نرمافزار به تحلیل آن میپردازد. چالش اساسی وارسی مدل در سیستمهای پیچیده و بزرگ که دارای فضای حالت گسترده و یا نامحدود میباشند، مشکل انفجار فضای حالت (کمبود حافظه در تولید همه حالتهای ممکن) است. الگوریتم جنگل تصادفی که قادر به کشف دانش است با انتخاب تعداد محدودی مسیر امیدبخش به مقابله با این مشکل میپردازد. درروش پیشنهادی، ابتدا مدل کوچکی از سیستم با استفاده از زبان رسمی سیستم توصیف گراف (GTS) ایجاد و از فضای حالت مدل کوچک، مجموعهای آموزشی ایجاد میشود. مجموعه آموزشی تولیدشده در اختیار الگوریتم جنگل تصادفی قرار داده میشود تا روابط منطقی موجود در آن شناسایی و کشف شوند. سپس از دانش بهدستآمده جهت پیمایش هوشمند و غیر کامل فضایِ حالتِ مدلِ بزرگ استفاده میشود. رویکرد پیشنهادی در ابزار GROOVE که از ابزار متنباز برای طراحی و بررسی مدل سیستمهای تبدیل گراف است، اجراشده است. نتایج نشان میدهند که روش پیشنهادی علاوه بر افزایش هوشمندی فرایند وارسی مدل، نیاز به تنظیم پارامترهای اولیه کمتری دارد. رویکرد پیشنهادی بر روی چند مسئله شناخته شده اجرا شده است. نتایج آزمایش های تجربی نشان میدهند روش پیشنهادی در مقایسه با روش های قبلی متوسط زمان اجرا، تعداد حالتهای پیمایش شده و دقت عملکرد بهتری دارد.
کلیدواژههای فارسی مقاله
تأیید سیستمهای نرمافزاری، کشف دانش، انفجار فضای حالت، وارسی مدل،
عنوان انگلیسی
Checking Reachability Property in Complex Concurrent Software Systems with a Knowledge Discovery Approach
چکیده انگلیسی مقاله
The model checking technique is a formal and effectual way in verification of software systems. By generation and investigation of all model states, it analyses the software systems. The main issue in the model checking of the complicated systems having wide or infinite state space is the lack of memory in generation of all states which is referred to as "state space explosion". The Random Forest algorithm which is capable of knowledge discovery faces the above-cited problem by selecting a few promising paths. In our suggested method, first a small model of the system is developed by the formal language of graph transformation system (GTS). A training data set is created from the small state space. The generated training data set is made available to the Random Forest algorithm to detect and discover the logical relationships existent in it. Then, the knowledge acquired in this way is used in the smart and incomplete exploration of the large state space. The proposed approach is run in GROOVE which is an open source tool for designing and studying the model of graph transformation systems. The results indicate that the suggested method in accordance with the two criteria (average running time and the number of explored states) performs better compared with the other approaches.
کلیدواژههای انگلیسی مقاله
تأیید سیستمهای نرمافزاری, کشف دانش, انفجار فضای حالت, وارسی مدل
نویسندگان مقاله
جعفر پرتابیان |
دانشکده مهندسی کامپیوتر، واحد لامرد، دانشگاه آزاد اسلامی، لامرد، ایران.
کرم الله باقری فرد |
دانشکده فنی و مهندسی، واحد یاسوج، دانشگاه آزاد اسلامی، یاسوج، ایران.
وحید رافع |
دانشکده فنی و مهندسی، گروه مهندسی کامپیوتر، دانشگاه اراک، اراک، ایران.
حمید پروین |
دانشکده مهندسی کامپیوتر، واحد نورآباد ممسنی، دانشگاه آزاد اسلامی، نورآباد ممسنی، ایران.
صمد نجاتیان |
گروه مهندسی برق، واحد یاسوج، دانشگاه آزاد اسلامی، یاسوج، ایران.
نشانی اینترنتی
https://jscit.nit.ac.ir/article_147496_e654d0960024674f98195a5c86759eb4.pdf
فایل مقاله
فایلی برای مقاله ذخیره نشده است
کد مقاله (doi)
زبان مقاله منتشر شده
fa
موضوعات مقاله منتشر شده
نوع مقاله منتشر شده
برگشت به:
صفحه اول پایگاه
|
نسخه مرتبط
|
نشریه مرتبط
|
فهرست نشریات