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

تکنیک وارسی مدل، روشی رسمی و موثر جهت تایید سیستم های نرم افزاری  است که با تولید  و بررسی همه حالت­های  ممکن مدلی از سیستم نرم افزار به تحلیل آن می­پردازد. چالش اساسی وارسی مدل در سیستم های پیچیده و بزرگ که دارای فضای حالت گسترده و یا نامحدود می باشند، مشکل انفجار فضای حالت (کمبود حافظه در تولید همه حالت های ممکن) است. الگوریتم جنگل تصادفی  که قادر به کشف دانش است با انتخاب تعداد محدودی مسیر امیدبخش به مقابله با این مشکل می­پردازد. درروش پیشنهادی، ابتدا مدل کوچکی از سیستم با استفاده از زبان رسمی سیستم توصیف گراف (GTS) ایجاد و از فضای حالت  مدل کوچک، مجموعه ای آموزشی  ایجاد می شود. مجموعه آموزشی تولیدشده در اختیار الگوریتم جنگل تصادفی قرار داده می شود تا روابط منطقی موجود در آن شناسایی و کشف شوند. سپس از دانش به دست آمده جهت پیمایش  هوشمند و غیر کامل فضای حالت مدل بزرگ استفاده می شود. رویکرد پیشنهادی در ابزار GROOVE که از ابزار متن باز برای طراحی و بررسی مدل سیستم های تبدیل گراف است، اجراشده است. نتایج نشان می دهند که روش پیشنهادی  علاوه بر افزایش هوشمندی فرایند وارسی مدل، نیاز به تنظیم پارامترهای اولیه کمتری دارد. رویکرد پیشنهادی بر روی چند مسئله شناخته شده اجرا شده است. نتایج آزمایش های تجربی نشان می­دهند روش پیشنهادی در مقایسه با روش های قبلی متوسط زمان اجرا، تعداد حالت­های پیمایش شده و دقت عملکرد بهتری دارد.

کلیدواژه ها:

تایید سیستم های نرم افزاری ، کشف دانش ، انفجار فضای حالت ، وارسی مدل