ارائه يك حل كننده محدوديت با امكان تعيين دامنه براي متغيرها با انواع داده اي پيچيده

كارشناسي ارشد

توسعه سيستم هاي نرم افزاري بزرگ يك فرايند پيچيده و مستعد خطا است. نزديك به سه دهه تجربه ثابت كرده است كه آزمون نرم افزار يك روش مؤثر براي اطمينان از كيفيت نرم افزار، از طريق آشكارسازي خطاها است. يكي از وظايف مهم هنگام آزمون نرم افزار، توليد داده هاي آزمون مناسب است. روش هاي زيادي براي هدايت فرايند توليد داده هاي آزمون توسعه داده شده اند كه از ميان آن ها مي توان به آزمون كانكاليك اشاره كرد. از لحاظ نظري، آزمون كانكاليك مي تواند به كمك يك حل كننده محدوديت قوي، پوشش مسير بالايي را فراهم كند. اما حل كننده هاي محدوديت موجود، داراي كاستي هايي هستند. يكي از اين كاستي ها، تنوع انواع داده اي پشتيباني شده توسط آن ها است. اغلب حل‌كننده هاي محدوديت، از محدوديت هاي مسير شامل متغيرهايي با نوع داده اي پيچيده نظير رشته ها، آرايه ها و ساختارها پشتيباني نكرده و قادر به حل كردن محدوديت هاي مسير شامل فراخواني هاي توابع جعبه سياه، توابعي كه كد آنها در دسترس نيست، نيستند. مسئله ديگر اين است كه تمامي حلكننده هاي محدوديت موجود، يك مقدار براي هريك از متغيرهاي حاضر در محدوديت مسير توليد كرده و از پوشش دامنه مناسبي برخوردار نيستند كه اين امر موجب مي شود تا بسياري از خطاهاي پنهان برنامه كشف نشده باقي بمانند. در اين رساله سعي شده است تا به منظور رفع كاستي هاي حل كننده هاي محدوديت موجود، روشي براي توليد يك حل كننده محدوديت ارائه شود. در روش ارائه شده، متغيرها از نوع رشته، آرايه اي از كاراكترها درنظر گرفته شده و در راستاي حل محدوديت هاي از نوع رشته، سه گام تعيين طول رشته ها، برآورده كردن محدوديت هاي ناشي از كاراكترهاي ثابت و برآورده كردن محدوديت هاي ناشي از عملگرها برداشته مي شود. در راستاي حل محدوديت هاي از نوع آرايه نيز دو گام برآورده كردن محدوديت هاي ناشي از ويژگي هاي ضمني آرايه نظير اندازه آرايه و برآورده كردن محدوديت ها در خصوص مقادير عناصر آرايه برداشته مي شود. در راستاي حل محدوديت هاي از نوع ساختار نيز براي هر فيلد ساختار، به طور جداگانه، داده هايي از يك نوع خاص توليد مي شود. نحوه برخورد ما با فراخواني هاي توابع جعبه سياه موجود در محدوديت مسير نيز بدين صورت است كه به جاي هر يك از توابع فراخواني شده، دامنه خروجي هايي كه تابع قادر به پذيرش آن ها است را قرار مي دهيم. به منظور ارزيابي نيز حل كننده محدوديت پيشنهادي از لحاظ انواع داده اي پشتيباني شده، موفقيت در حل محدوديت هاي مسير، زمان اجرا و پوشش دامنه، با پنج مورد از شناخته شده ترين، جديدترين و قوي ترين حل كننده هاي محدوديت موجود، CVC4، S3، Yices2، Z3 و Z3str3، مورد مقايسه و ارزيابي قرار گرفته است. نتايج به دست آمده از ارزيابي، حاكي از آن است كه حل كننده محدوديت پيشنهادي توانسته است تا حد زيادي معيارهاي نام برده را بهبود ببخشد.

196517

دانشگاه علم و صنعت ايران

-

مهندسي كامپيوتر

سعيد پارسا