ارائه­ دهنده:

  استاد راهنما:

دکتر سعید پارسا


هیات داوران:
دکتر محمد عبداللهی ازگمی
دکتر مجتبی وحیدی اصل

زمان:
دوشنبه ۱۴۰۰/۰۳/۳۱

خانم نگار فتحی دانشجوی کارشناسی ارشد آقای دکتر سعید پارسا روز دوشنبه ۳۱ خرداد ماه ساعت ۱۷:۰۰ از پروژه کارشناسی ارشد خود تحت عنوان "ارائه یک حل‏کننده محدودیت با امکان تعیین دامنه برای متغیرها با انواع داده‏ای پیچیده " دفاع خواهند نمود.

چکیده پایان نامه:
 توسعه سیستم‏های ‏نرم‏افزار‏ی بزرگ یک فرایند پیچیده و مستعد خطا است. خطاها ممکن است در هر مرحله از توسعه ‏نرم‏افزار‏ رخ دهند. این خطاها، درصورت عدم شناسایی و حذف به‏موقع، ‏می‏توانند‏ از نظر زمانی و مالی ضرر زیادی به‏بار آورند. نزدیک به ‏سه دهه تجربه ثابت کرده‏است که ‏آزمون ‏نرم‏افزار‏ یک روش مؤثر برای اطمینان از کیفیت ‏نرم‏افزار،‏ از طریق آشکارسازی خطاها است. یکی از وظایف مهم هنگام ‏آزمون ‏نرم‏افزار،‏ تولید داده‏های ‏آزمون مناسب است. روش‏های زیادی برای هدایت فرایند تولید داده‏های ‏آزمون توسعه داده شده‏اند که از میان آن‏ها می‏توان به آزمون کانکالیک اشاره کرد. از لحاظ تئوری، آزمون کانکالیک می‌تواند به کمک یک حل‌کننده محدودیت قوی، پوشش مسیر بالایی را فراهم کند. اما چنین حل‌کننده محدودیتی وجود ندارد. حل‌کننده‏های محدودیت موجود، دارای نقاط ضعفی هستند که می‏توان به تنوع انواع داده‏ای پشتیبانی‏شده توسط آن‏ها اشاره کرد. اغلب حل‌کننده‏های محدودیت موجود، از محدودیت‏های مسیر شامل متغیرهایی با نوع داده‏ای پیچیده نظیر رشته‏ها، آرایه‏ها و ساختارها پشتیبانی نکرده و قادر به حل‏کردن محدودیت‏های مسیر شامل فراخوانی‏های توابع جعبه سیاه، توابعی که کد آن‏ها در دسترس نیست، نیستند. مسئله دیگر این است که تمامی حل‏کننده‏های محدودیت موجود، یک مقدار برای هریک از متغیرهای حاضر در محدودیت مسیر تولید کرده و از پوشش دامنه مناسبی برخوردار نیستند که این امر موجب می‎شود تا بسیاری از خطاهای پنهان برنامه کشف‏نشده باقی بمانند. در این رساله سعی شده‏است تا به‏منظور رفع نقاط ضعف‏ حل‏کننده‏های محدودیت موجود، روشی برای تولید یک حل‏کننده محدودیت ارائه شود. به‏منظور ارزیابی نیز حل‏کننده محدودیت پیشنهادی از لحاظ انواع داده‏ای پشتیبانی‏شده، موفقیت در حل محدودیت‏های مسیر، زمان اجرا و پوشش دامنه، با پنج مورد از شناخته‏شده‏ترین، جدیدترین و قوی‏ترین حل‏کننده‏های محدودیت، CVC۴، S۳، Yices۲، Z۳ و Z۳str۳، مورد مقایسه و ارزیابی قرار گرفته‏است. نتایج به‏دست‏آمده از ارزیابی، حاکی از آن است که حل‏کننده محدودیت پیشنهادی توانسته‏است تا حد زیادی معیارهای نام‏برده را بهبود ببخشد.
واژه‌های کلیدی: حل‏کننده محدودیت، پوشش دامنه، انواع داده‏ای پیچیده