Model Verification of Dynamic Software Product Lines

Dynamic Software Product Lines (DSPLs) extend the concept of Software Product Lines enabling adaptation at runtime according to context changes. Such dynamic behavior is typically designed using adaptation rules, context-triggered actions responsible for features activation and deactivation at runtime. The erroneous specification and the interleaving of adaptation rules (i.e., the parallel execution of adaptation rules) can lead DSPL to reach an undesired (improperly or defective) product configuration at runtime. Thus, in order to improve the reliability of DSPL behavior, design faults must be rigorously identified and eliminated in the early stages of DSPL development. In this paper, we address this issue introducing Dynamic Feature Transition Systems (DFTSs) that allow the modeling and formal verification of the DSPLs adaptive behavior. These transition systems are derived from the adaptation rules and a Context Kripke Structure, which is a context evolution model. Furthermore, we formally define five properties that can be used to identify existing design faults in DSPL design. Aiming to assess the feasibility of our approach, a feasibility study was conducted using two DSPLs, Mobile Visit Guides and Car. In both cases, design faults were automatically detected indicating that our formalism can help in the detection of design faults in the DSPLs adaptive behavior.