25174

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

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

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

1397

1400/03/31

سعيد پارسا

-

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

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

1400/06/09

A Constraint Solver to Determine the Domain for Variables with Complex Data Types

6/21/2022 12:00:00 AM

The development of large software systems is a complex and fault-prone process. Faults may occur at any stage of software development. If these faults are not identified and eliminated in time, they can cause a lot of damage in terms of time and money. Nearly three decades of experience have proven that software testing is an effective way to ensure software quality by detecting faults. One of the most important tasks when testing software is to generate appropriate test data. Many methods have been developed to lead the process of generating test data, among which we can mention the concolic testing. Theoretically, the concolic testing can provide high path coverage with the help of a strong constraint solver. But there is no such constraint solver. Existing constraint solvers have shortcomings. One of these shortcomings is the variety of data types supported by these constraint solvers. Most constraint solvers do not support path constraints involving variables with complex data types such as strings, arrays, and structs. And they are not able to solve path constraints involving the black-box function calls, functions whose code is not available. Another issue is that all existing constraint solvers generate a value for each variable present in the path constraint and do not have adequate domain coverage, which leaves many latent faults of the program undetected. In this thesis, to eliminate the shortcomings of existing constraint solvers, an attempt has been made to present a method for producing a constraint solver. In order to evaluate, the proposed constraint solver has been compared and evaluated in terms of supported data types, success in solving path constraints, runtime, and domain coverage with five of the most well-known, newest, and powerful existing constraint solvers, CVC4, S3, Yices2, Z3, and Z3str3. The evaluation results indicate that the proposed constraint solver has been able to greatly improve the mentioned criteria.

حل كننده محدوديت , پوشش دامنه , انواع داده اي پيچيده

Constraint Solver , Domain Coverage , Complex Data Types