A Framework for Model-Based Specification and Verification in Feature-Oriented Software Product Lines

At the heart of Product Line Engineering (PLE) lies the feature model, which describes how features can be combined to create customized variability and commonality in the development of reconfigurable cyber-physical systems. Since standardized processes are key to high-quality product development, managing their variability should align with PLE principles and regulatory standards. However, misconfigurations frequently arise due to the complexity of these standardized processes leading to potentially hazardous conditions. Therefore, containment verification of each configuration in variability management remains a complex task, that requires extensive analysis and considerable effort. We introduce a containment verification approach to determine whether a certain product configuration is consistent with the specification defined in a feature model. Our method provides a model-based architectural analysis that identifies misconfiguration against the architecture and the potential damage scenarios of their mitigations. To facilitate this task, we model the security architecture and requirements in an Eclipse-based IDE that supports all phases of feature-oriented software development for PLE. Subsequently, the proposed approach performs automated transformation of these models, using the Acceleo transformation language, into formal constraints and descriptions, in order to leverage the analytical power of model-checking techniques. The formal verification of completeness, consistency, and conflict is carried out using the NuSMV model checker. In case a counterexample is produced, a change impact analysis is performed for the identification of problems and their resolutions. We conducted a case study to evaluate the accuracy of the verification results and the inferred model transformations.