فهرست نشریات علمی دسترسی آزاد ایران

آزمون نرم‌افزار یک موضوع مهم و لازم در فرآیند توسعه هر نرم‌افزاری می‌باشد. امروزه بخش عمده‌ای از آزمون نرم‌افزار به شیوه خودکار انجام می‌شود. در آزمون خودکار نرم‌افزار موانعی می‌توانند وجود داشته باشند که آزمون را با مشکل مواجه کنند. از این موانع، می‌توان به وجود مسیرهای غیرقابل اجرا در گراف جریان کنترلی حاصل از کدهای نرم‌افزار تحت آزمون اشاره کرد. مسیرهای غیرقابل اجرا، مسیرهایی هستند که با هیچ ورودی نمی‌توان از آنها عبور کرد. وجود چنین مسیرهایی، می‌تواند در حوزه‌های مختلف، مانند تولید داده آزمون، امنیت و مانند آن مشکلاتی را به وجود آورد و باعث هدر رفت منابع شود. برای پیشگیری از مشکلات ذکر شده، تشخیص مسیرهای غیرقابل اجرا بسیار مهم می‌باشد. اما تشخیص این مسیرها در نرم‌افزارهای بزرگ، به دلیل حجم زیاد کدها و زیاد بودن تعداد مسیرها در گراف جریان کنترلی، می‌تواند کاری زمانبر باشد. در روش ارائه شده در این مقاله، سرعت تشخیص مسیرهای غیرقابل اجرا با بکارگیری الگوریتم‌های یادگیری تقویتی بهبود داده شده است. در این روش سرعت حل‌کننده 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 برابر افزایش یافته است.