استفاده از یادگیری تقویتی جهت افزایش سرعت حل‌کننده‌های 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 برابر افزایش یافته است.

کلیدواژه‌ها

موضوعات

عنوان مقاله [English]

Improve methods of infeasible path detection by SMT solvers in software testing using reinforcement learning

نویسندگان [English]

  • Majid Feyzi
  • Mohammad Mehdi Esnaashari
Faculty of Computer Engineering, K.N Toosi University of Technology, Tehran, Iran.
چکیده [English]

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.

کلیدواژه‌ها [English]

  • Automated software testing
  • Infeasible paths
  • SMT solver
  • Z3 solver
  • Reinforcement learning
  • DQN

مراجع

[1] P. Ammann and J. Offutt, Introduction to Software Testing. Cambridge, U.K.: Cambridge Univ. Press, 2016, doi: 10.1017/9781316771273.
[2] B. Beizer, Software Testing Techniques. New York, NY, USA: Van Nostrand Reinhold, 1990.
[3] H. Farzaneh, S. Bakhshayeshi, R. Ebrahimi Atani, and A. Shahbahrami, “A survey on test data generation techniques based on Mutation Testing,” Soft Comput. J., vol. 2, no. 1, pp. 72-85, 2013, dor: 20.1001.1.23223707.1392.2.1.61.5 [In Persian].
[4] Y.-W. Wang, Y. Xing, and X.-Z. Zhang, “A method of path feasibility judgment based on symbolic execution and range analysis,” Int. J. Future Gener. Commun. Netw., vol. 7, no. 3, pp. 205-212, 2014, doi: 10.14257/ijfgcn.2014.7.3.19.
[5] H. Zhu, D. Jin, Y. Gong, Y. Xing, and M. Zhou, “Detecting interprocedural infeasible paths based on unsatisfiable path constraint patterns,” IEEE Access, vol. 7, pp. 15040-15055, 2019, doi: 10.1109/ACCESS.2019.2894593.
[6] S. Jiang et al., “An approach for detecting infeasible paths based on a SMT solver,” IEEE Access, vol. 7, pp. 69058-69069, 2019, doi: 10.1109/ACCESS.2019.2918558.
[7] L. de Moura and N. Bjorner, “Z3: An efficient SMT solver,” in Proc. Int. Conf. Tools Algorithms Constr. Anal. Syst., 2008, pp. 337-340, doi: 10.1007/978-3-540-78800-3_24.
[8] C. Barrett and C. Tinelli, “Satisfiability modulo theories,” in Handbook of Model Checking, Springer, 2018, pp. 305-343, doi: 10.1007/978-3-319-10575-8_11.
[9] M. Balunovic, P. Bielik, and M. Vechev, “Learning to solve SMT formulas,” Adv. Neural Inf. Process. Syst., vol. 31, 2018.
[10] S. Anand, P. Godefroid, and N. Tillmann, “Demand-driven compositional symbolic execution,” in Proc. Int. Conf. Tools Algorithms Constr. Anal. Syst., 2008, pp. 367-381, doi: 10.1007/978-3-540-78800-3_28.
[11] J. Scott, F. Mora, and V. Ganesh, “BanditFuzz: Fuzzing SMT solvers with reinforcement learning,” University of Waterloo, Waterloo Research, 2020.
[12] S. Jeon and J. Moon, “Dr. PathFinder: Hybrid fuzzing with deep reinforcement concolic execution toward deeper path-first search,” Neural Comput. Appl., vol. 34, pp. 10731-10750, 2022, doi: 10.1007/s00521-022-07008-8.
[13] M. Hajibaba and S. Parsa, “Software Fault Localization using Cross Entropy and N-gram Models,” Soft Comput. J., vol. 2, no. 1, pp. 44-59, 2013, dor: 20.1001.1.23223707.1392.2.1.59.3 [In Persian].
[14] S. Ding, H.B.K. Tan, and K.P. Liu, “A survey of infeasible path detection,” in Proc. 7th Int. Conf. Eval. Novel Approaches Softw. Eng. (ENASE), 2012, pp. 43-52.
[15] S. Jang, H.-Y. Kim, Y.-H. Choi, and T.-M. Chung, “A study of advanced hybrid execution using reverse traversal,” in Proc. 2011 Int. Conf. Inf. Manag. Innov. Manag. Ind. Eng., vol. 2, 2011, pp. 557-559, doi: 10.1109/ICIII.2011.278.
[16] H. Ghorbani Moghadam, B. Jamasb, and H. Dehdashti Jahromi, “Review on security requirements in the software production process,” Soft Comput. J., vol. 10, no. 2, pp. 72-83, 2022, doi: 10.22052/scj.2022.242857.0 [In Persian]
[17] B. Barhoush and I. Alsmadi, “Infeasible paths detection using static analysis,” Res. Bull. Jordan ACM, vol. 2, no. 3, pp. 120-126, 2013.
[18] N. Malevris, D. Yates, and A. Veevers, “Predictive metric for likely feasibility of program paths,” Inf. Softw. Technol., vol. 32, no. 2, pp. 115-118, 1990, doi: 10.1016/0950-5849(90)90110-D.
[19] D. Yates and N. Malevris, “Reducing the effects of infeasible paths in branch testing,” ACM SIGSOFT Softw. Eng. Notes, vol. 14, no. 8, pp. 48-54, 1989, doi: 10.1145/75309.75315.
[20] SMT-LIB, Accessed: Feb. 6, 2022, [Online]. Available: https://smtlib.cs.uiowa.edu/.
[21] R.S. Sutton and A.G. Barto, Reinforcement Learning: An Introduction. London, U.K.: The MIT Press, 2018.
[22] E.J. Weyuker, “The applicability of program schema results to programs,” Int. J. Comput. Inf. Sci., vol. 8, no. 5, pp. 387-403, 1979, doi: 10.1007/BF00995175.
[23] D. Gong and X. Yao, “Automatic detection of infeasible paths in software testing,” IET Softw., vol. 4, no. 5, pp. 361-370, 2010, doi: 10.1049/iet-sen.2009.0092.
[24] D. Kundu, M. Sarma, and D. Samanta, “A UML model-based approach to detect infeasible paths,” J. Syst. Softw., vol. 107, pp. 71-92, 2015, doi: 10.1016/j.jss.2015.05.007.
[25] G. Brockman, V. Cheung, L. Pettersson, J. Schneider, J. Schulman, J. Tang and W. Zaremba, “OpenAI Gym,” arXiv preprint, arXiv:1606.01540, 2016.
[26] V. Mnih et al., “Human-level control through deep reinforcement learning,” Nature, vol. 518, pp. 529-533, 2015, doi: 10.1038/nature14236.

فایل ها

سابقه مقاله

  • تاریخ دریافت: 20 شهریور 1402
  • تاریخ بازنگری: 06 آذر 1402
  • تاریخ پذیرش: 26 دی 1402

هم رسانی

ارجاع به این مقاله

آمار