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

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

جستجوی پرتو، روش رسمی، وارسی مدل، تبدیل گراف