عنوان پایان‌نامه
بهینه سازی آزمونگر ربکا
- رشته تحصیلی
- مهندسی کامپیوتر -نرم افزار
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 41788;کتابخانه مرکزی پردیس 2 فنی شماره ثبت: E 1608
- تاریخ دفاع
- ۱۴ تیر ۱۳۸۸
- دانشجو
- هومن بنده مقدم
- چکیده
- چکیده با تولید روزافزون سیستمهای حساس و بحرانی، نیاز به درستی¬یابی آنها بیش از پیش احساس می¬شود. حتی در سیستمهای با حساسیت کمتر نیز نیاز به بررسی کامل درستی وجود دارد. در این میان، درستی¬یابی صوری سیستمهای کامپیوتری، اعم از سخت افزاری و نرم افزاری، از اهمیت ویژه¬ای برخوردار می¬باشد. درستی¬یابی سیستمها شامل مدل کردن آنها و سپس اعمال روشهای درستی¬یابی روی مدل به دست آمده از سیستم می¬باشد. زبان ربکا یکی از زبانهایی است که برای مدلسازی سیستمهای همروند و واکنشی به ویژه سیستمهای توزیع شده و پروتوکلهای نرم¬افزاری متشکل از پردازه‌های ناهمگام استفاده می¬شود. از طرف دیگر، درستی¬یابی صوری از دو روش قابل انجام است، روش الگوریتمی یا آزمون مدل و روش استنتاجی . در روش استنتاجی، با استفاده از قضیه¬ها و اصول ریاضی سعی در اثبات درستی سیستم می¬کنند. این روش ا نیاز به خبرگی خاصی دارد. در روش آزمون مدل، علاوه بر مدل سیستم، خصوصیاتی از مدل که درستی آنها باید ارزیابی شود نیز توصیف می¬شود. این خصوصیات به دو روش منطق زمانی خطی(LTL) و منطق محاسبات درختی (CTL) بیان می¬شوند. در این پروژه، در قدم نخست الگوریتمها و روشهای موجود برای درستی¬یابی از طریق آزمون مدل با استفاده از CTL بررسی شده است و الگوریتمی با ترکیب خصوصیات و مزایای سایر الگوریتمها پس از تطبیق با خصوصیات ربکا، پیاده سازی شده است. سپس با بررسی روشهای موجود در زمینه بهینه سازی، راهکارهایی برای بهبود کارآیی این ابزار به کار رفته است. دراین بخش با استفاده از روش برش دادن و تحلیل وابستگی داده ای حجم فضای حالت کاهش داده شده است. در این ابزار، از روش درستی یابی الگوریتمی و خودکار، یعنی آزمون مدل استفاده شده است که برای اطمینان از عملکرد سیستم، تمام حالات قابل دستیابی به طور خودکار تولید و بررسی می-شوند
