ناهید سلیمی - دانشجوی کارشناسی ارشد دانشکده فنی و مهندسی، گروه مهندسی کامپیوتر، دانشگاه اراک
وحید رافع - دانشیار دانشکده فنی و مهندسی، گروه مهندسی کامپیوتر، دانشگاه اراک

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

وارسی مدل، انفجار فضای حالت، سیستم تبدیل گراف، الگوریتم ژنتیک فازی، بن بست