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

آزمون خودکار نرم افزار امری ضروری در فرایند توسعه هر نرم افزاری می باشد. در آزمون خودکار ممکن است موانعی وجود داشته باشند که آزمون را با مشکل مواجه نمایند. یکی از این موانع، وجود مسیرهای غیرقابل اجرا در گراف جریان کنترلی بدست آمده از کدهای نرم افزار تحت آزمون است. وجود چنین مسیرهایی، می تواند در تولید داده آزمون، امنیت و... مشکلاتی را به وجود آورد و باعث هدر رفت منابع شود.به منظور پیشگیری از این مشکلات، تشخیص مسیرهای غیرقابل اجرا بسیار حیاتی است. اما در نرم افزارهای بزرگ، تشخیص این مسیرها به دلیل زیاد بودن حجم کدها و به تبع آن زیاد بودن مسیرها در گراف جریان کنترلی، کاری زمانبر است. در این مقاله، روشی ارائه شده که با به کارگیری یادگیری تقویتی می تواند سرعت تشخیص مسیرهای غیرقابل اجرا را افزایش دهد. در این روش با استفاده از عامل DQN ، سرعت حل کننده SMT، افزایش داده می شود. در واقع در این مقاله نشان داده شده است که می توان با استفاده از یادگیری تقویتی، تاکتیک های ارائه شده توسط SMT را یاد گرفت و سپس با اعمال تاکتیک های یادگیرفته شده، سرعت حل را افزایش داد. بدین ترتیب سرعت تمامی روش هایی که از این ابزار برای تشخیص مسیرهای غیرقابل اجرا استفاده می کنند نیز افزایش می یابد. روش ارائه شده در این مقاله بر روی منطق های QF_NRA و QF_NIA آزمایش شده است. آزمایشاتی که انجام شده نشان داده است که با استفاده از روش پیشنهادی، می توان سرعت حل کننده SMT را تا ۴/۷ برابر افزایش داد.

کلیدواژه ها:

آزمون خودکار نرم افزار ، مسیرهای غیرقابل اجرا ، حل کننده SMT ، حل کننده Z۳ ، یادگیری تقویتی ، DQN