A Theory of Software Product Line Refinement

Paulo Borba, Leopoldo Teixeira, Rohit Gheyi

Abstract for ICTAC'2010

To safely derive and evolve a software product line, it is important to have a notion of product line refactoring and its underlying refinement notion, which assures behavior preservation. In this paper we present a general theory of product line refinement by extending a previous formalization with explicit interfaces between our theory and the different languages that can be used to create product line artifacts. More important, we establish product line refinement properties that justify stepwise and compositional product line development and evolution.

PVS Specification for ICTAC'2010

• PVS specification file (SPLrefinement.pvs)
• PVS Proof file (SPLrefinement.prf)

Abstract for TCS'2011

To safely derive and evolve a software product line, it is important to have a notion of product line refactoring and its underlying refinement notion, which assures behavior preservation. In this paper we present a language independent theory of product line refinement, establishing refinement properties that justify stepwise and compositional product line development and evolution. Moreover, we instantiate our theory with the formalization of specific languages for product lines artifacts, and then introduce and prove soundness of a number of associated refinement transformation templates. This can be used to reason about specific product lines, and as a basis to derive comprehensive product line refactoring catalogues.

PVS Specification for TCS'2011

• All PVS files (see description below)
• SPLRefinement defines the general theory for SPL refinement
• AssetMapping defines asset mappings
• Assets defines generic assets
• ConfigurationKnowledge defines the specific configuration knowledge language
• FeatureModel defines the specific feature model language
• FeatureModelRefinements defines some lemmas that are useful during soundness proof for the transformations, regarding feature model refinements
• FeatureModelSemantics defines properties for the feature models
• Formula_ defines the propositional formulae language we use on feature models and configuration knowledge
• FormulaTheory defines properties and useful functions for propositional formulae
• maps is the parameterized theory used for defining asset mappings
• Name defines feature names and product configurations
• set_aux_lemmas and set_comp_lemmas define auxiliary lemmas for sets and set comprehensions that are useful for the other theories
• SpecificSPL is the theory that instantiates (using theory interpretation) the general theory with the specific languages

• Additional Proofs for Lemmas and Theorems