ارایه راهکاری جهت مقابله با مشکل انفجار فضای حالت در سیستم های تبدیل گراف با استفاده از الگوریتم های پرندگان و جستجوی گرانشی

وارسی مدل، یک روش خودکار و راهکاری مناسب به منظور درستی یابی سیستم های نرم افزاری مطمین است. در این سیستم ها، نمی توانریسک بروز خطا را حتی در فرآیند تست پذ یرفت و لذا لازم است فرآیند درستی یابی، قبل از پیاده ساز ی و در سطح مدل انجام شود. سیستم هایتبدیل گراف، از پرکاربردترین سیستم های مدلسازی رسمی و راهکاری مناسب به منظور مدلسازی و وارسی سیستم های پیچیده هستند. اما اینسیستم ها در فرآیند وارسی مدل از مشکل انفجار فضای حالت رنج می برند که در صورت گسترده بودن ابعاد مسیله و لذا بزرگ شدن فضای حالتمدل، سیستم با کمبود حافظه مواجه می شود . لذا هدف از این پژوهش، پیشنهاد راهکاری جهت مقابله با این مشکل در فرآیند وارسی سیستم هایتبدیل گراف است. راهکارهای ارایه شده، به جای تولید کل فضای حالت، آن را در جهت رسیدن به یک حالت خطا به طور مثال بن بست، هدایتمی کنند. راهکار پیشنهاد ی بر مبنای الگوریتم پرندگان طراحی شده و برای جلوگیری از مشکل به دام افتادن در بهینه های محلی که مشکل اصلیاین الگوریتم است، با الگور یتم جستجوی گرانشی که دارای قدرت خوبی در جستجو ی محلی است، ترکیب شده است. در نهایت به منظور ارزیابینتایج راهکارهای ارایه شده، این راهکارها در ابزار Groove- از ابزارهای مدلسازی تبدیل گراف- پیاده سازی شده اند.

Keywords:

وارسی مدل , سیستم تبدیل گراف , انفجار فضای حالت , الگوریتم پرندگان , الگوریتم جستجوی گرانشی