Goal-conflict identification based on local search and fast boundary-condition verification based on incremental satisfiability filter

Identifying boundary conditions (BCs) is of fundamental importance for goal-conflict analysis. BCs are able to capture particular combinations of circumstances that make some special conflicts, namely goal divergences, in which the goals of the requirement cannot be satisfied as a whole. Unfortunately, existing approaches only handle small-scale cases within a reasonable running time and do not consider how to search more general BCs because of the search space explosion and the high computational cost of verifying BCs. In this paper, we observed that the BCs identified by the state-of-the-art (SOTA) approach share similarities in structure. It inspires us to develop a BC identification approach, named LOGION, based on local search, to better exploit the similarity in structures. Specifically, we utilize the structural similarity of BCs to construct the neighborhood relation of our local search algorithm. Besides, we design strengthening and weakening operators of formulae to capture the semantics of more general BCs in local searching. In order to boost the BC verification, we propose a lasso-based incremental satisfiability filter (LISF). The primary intuition behind LISF is using trace checking as a light-weight pre-checking, and if it is not successful, to call the satisfiability checking. We conduct extensive experiments to evaluate LOGION, comparing against SOTA approaches. Experimental results show that LOGION produces about 1 order of magnitude more general BCs than the SOTA approaches. It is also shown that LISF significantly boosts the speed, especially for large-scale cases (up to about 1 order of magnitude faster on average).