|
Title
|
ارائه جستجوی پرتو بهبودیافته برای وارسی مدل سیستم های تبدیل گراف
|
|
Type of Research
|
Presentation
|
|
Keywords
|
جستجوی پرتو، روش رسمی، وارسی مدل، تبدیل گراف
|
|
Abstract
|
وارسی مدل یک روش رسمی برای تحلیل خودکار سیستم های نرم افزاری است که با تولید و بررسی همه حالت های ممکنِ مدلی از سیستم نرم افزاری به تحلیل آن می پردازد. مشکل وارسی مدل این است که در سیستم های پیچیده با مشکل انفجار فضای حالت (کمبود حافظه در تولید همه حالت های ممکن) مواجه می شود. جستجوی پرتو روشی است که با پیمایش سطح به سطح و انتخاب تعداد محدودی حالت امیدبخش در هر سطح به مقابله با این مشکل می پردازد. حالتی امیدبخش است که احتمال رسیدن به یک جواب از طریق این حالت، بیشتر از بقیه حالت ها باشد. با این همه، در این روش نیز ممکن است بعد از چندین سطح، به حالت هایی برسیم که احتمال رسیدن به جواب از طریق اینها، کمتر از حالت های انتخاب نشده در سطوح قبلی باشد. از این رو، در این مقاله راه حلی مبتنی بر جستجوی پرتو ارائه می کنیم که علاوه بر انتخاب تعدادی حالت امیدبخش در هر سطح، تعدادی حالت با میزان امیدبخشی کمتر و انتخاب شده از سطوح قبلی بعنوان حالت های پشتیبان نگهداری شوند. سپس، در سطوح بعدی و موقع انتخاب حالت های امیدبخش، این حالت های پشتیبان نیز مدنظر قرار بگیرند. برای ارزیابی کارایی روش ارائه شده، آن را در ابزار GROOVE – از ابزارهای وارسی مدل مبتنی بر زبان تبدیل گراف پیاده سازی می کنیم.
|
|
Researchers
|
Einollah Pira (First Researcher)
|