استفاده از یادگیری تقویتی جهت افزایش سرعت حل‌کننده‌های smt با هدف تشخیص سریع‌تر مسیرهای غیر‌قابل اجرا در نرم‌افزار

آزمون نرم‌افزار یک موضوع مهم و لازم در فرآیند توسعه هر نرم‌افزاری می‌باشد. امروزه بخش عمده‌ای از آزمون نرم‌افزار به شیوه خودکار انجام می‌شود. در آزمون خودکار نرم‌افزار موانعی می‌توانند وجود داشته باشند که آزمون را با مشکل مواجه کنند. از این موانع، می‌توان به وجود مسیرهای غیرقابل اجرا در گراف جریان کنترلی حاصل از کدهای نرم‌افزار تحت آزمون اشاره کرد. مسیرهای غیرقابل اجرا، مسیرهایی هستند که با هیچ ورودی نمی‌توان از آنها عبور کرد. وجود چنین مسیرهایی، می‌تواند در حوزه‌های مختلف، مانند تولید داده آزمون، امنیت و مانند آن مشکلاتی را به وجود آورد و باعث هدر رفت منابع شود. برای پیشگیری از مشکلات ذکر شده، تشخیص مسیرهای غیرقابل اجرا بسیار مهم می‌باشد. اما تشخیص این مسیرها در نرم‌افزارهای بزرگ، به دلیل حجم زیاد کدها و زیاد بودن تعداد مسیرها در گراف جریان کنترلی، می‌تواند کاری زمانبر باشد. در روش ارائه شده در این مقاله، سرعت تشخیص مسیرهای غیرقابل اجرا با بکارگیری الگوریتم‌های یادگیری تقویتی بهبود داده شده است. در این روش سرعت حل‌کننده smt به نام z3 با بهره‌گیری از عامل dqn، افزایش داده می‌شود. z3 ابزاری است که برای بررسی قابل حل بودن فرمول‌های ساخته شده از شرط‌های موجود در گراف جریان کنترلی در تشخیص مسیر‌های غیرقابل اجرا استفاده می‌شود. در واقع در این مقاله تاکتیک‌‌های ارائه شده توسط z3 با استفاده از یادگیری تقویتی یاد گرفته شده و سپس با انتخاب و اعمال تاکتیک‌های z3 براساس یادگیری انجام شده، سرعت حل z3 افزایش می‌یابد. با افزایش سرعت z3، سرعت تمامی روش‌ها و الگوریتم‌هایی که از این ابزار برای تشخیص مسیرهای غیرقابل اجرا استفاده می‌کنند نیز افزایش خواهد یافت. همچنین ابزار z3 در هر حوزهای که بتوان مسائل را به مساله بررسی صدق‌پذیری یک فرمول کاهش داد نیز کاربرد دارد و بهبود عملکرد آن در چنین حوزه‌هایی نیز می‌تواند موثر باشد. روش ارائه شده در این مقاله در منطق‌های qf_nra و qf_nia آزمایش شده است. در آزمایش‌های انجام شده، نشان داده شده است که با استفاده از روش پیشنهادی، سرعت z3 را می‌توان تا 4.7 برابر افزایش داد. همچنین در آزمایش‌های انجام شده با استفاده از این روش، سرعت z3 در منطق qf_nra، به طور میانگین 1.954 برابر و در منطق qf_nia، به طور میانگین 1.687 برابر افزایش یافته است.

improve methods of infeasible path detection by smt solvers in software testing using reinforcement learning

software testing is an important and necessary matter in the development process of any software. nowadays، an important part of software testing is performed automatically. in automated software testing، there may be obstacles that make the test difficult. one of these obstacles is the infeasible paths in the control flow graph obtained from the source code of the software under test. infeasible paths are paths that cannot be traversed by any input. the existence of such paths can cause problems in various fields such as test data generation، security and etc.، leading to a waste of resources. in order to prevent the mentioned problems، detection of infeasible paths can be very critical. but recognizing these paths in large software can be a time-consuming task due to the large amount of codes and the high number of paths in the control flow graph. in this article، a method is proposed that can increase the infeasible paths detection speed by applying reinforcement learning algorithms. in this method، the speed of the z3 smt solver has been increased by using the dqn agent. z3 is a tool used to check the satisfiability of formulas constructed from the conditions in the control flow graph for detecting infeasible paths. in fact، in this paper، the techniques provided by z3 are learned using reinforcement learning، and then by selecting and applying these techniques based on the learning performed، the solving speed increases. as the speed of the z3 tool increases، the speed of all algorithms and methods that use this tool to detect infeasible paths in control flow graphs will also increase. also، the z3 tool is applicable in any field where problems can be reduced to the satisfiability of a formula، and improving its performance in those fields can also be effective. the proposed method in this article has been tested on qf_nra and qf_nia logics. in the experiments، it is shown that using the proposed method، the speed of the z3 solver can be increased up to 4.7 times. furthermore، in the conducted experiments using this method، the speed of z3 increased by an average of 1.954 times in qf_nra logic and 1.687 times in qf_nia logic.