Interactive Prioritization of Software Requirements using the Z3 SMT Solver

Sammanfattning: Prioritization of software requirements is an important part of the requirements engineering process within the industry of software development. There are many different methods for achieving the most optimal order of software requirements, a list that shows in what order the requirements should be implemented. This degree project utilizes the SMT-based solver Z3 for an interactive prioritization algorithm. Previous studies have shown good results with another SMT-based solver called Yices. With the newer Z3 from Microsoft, the results have been improved further, and the tool is based on Python, and the framework for Z3 is called Z3PY. Experiments have been conducted on a set of different software requirements derived from a project in the healthcare industry and show that the Z3 solution is, in general, improving the requirements prioritization compared to other mentioned solutions in the study that has been tested on the same set of requirements. Results show that the Z3 solution outperformed the other SMT-based solution Yices by 2-4% regarding disagreement and by 3% regarding average distance. The results are significantly improved based on an ANOVA test with a p-value <= 0.05.