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

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