When evolving a software product line, it is often important to ensure that we do it in a safe way, ensuring that the resulting product line remains well-formed and that the behavior of existing products is not affected. To ensure this, one usually has to analyze the different artifacts that constitute a product line, like feature models, configuration knowledge and assets. Manually analyzing these artifacts can be time-consuming and error prone, since a product line might consists of thousands of products. Existing works show that a non-negligible number of changes performed in commits deal only with the configuration knowledge, that is, the mapping between features and assets. This way, in this paper, we propose a set of algebraic laws, which correspond to bi-directional transformations for configuration knowledge models, that we can use to justify safe evolution of product lines, when only the configuration knowledge model changes. Using a theorem prover, we proved all laws sound with respect to a formal semantics. We also present a case study, where we use these laws to justify safe evolution scenarios of a non trivial industrial software product line.
This work was partially supported by CNPq (grant 409335/2016-9) and FACEPE (APQ-0570-1.03/14), as well as INES 2.0, FACEPE grants PRONEX APQ-0388-1.03/14 and APQ-0399-1.03/17, and CNPq grant 465614/2014-0.