1. Feature Model (FM):

   • A feature model (FM) defines the products of a product line.
   • FM defines variations that programs can have in an SPL.
   • FM is a blueprint to allow user specify products declaratively.

2. Feature Diagrams (FD):

   • A FD is a tree.
   • Leaves are primitive features, while internal nodes are compound features.
   • Parent and child are containment relation (has …).
   • Order doesn’t matter

1. FDs are Grammars

   • Car := [Cr] Eng+ Tr CBody
   • Tr := Auto | Manual
   • Eng := Gas | Ele
   • Application defined by FD = Sentence defined by Grammar Car.

2. Grammars are compact representations of propositional formulas.

   • E := R S ; E ⇔ R ∧ S
   • R := g | h | i ; R ⇔ choose1(g, h, i)
   • S := a [b] c ; S ⇔ (a ∧ c) ∧ (b ==> S)

3. A feature model is a propositional formula = (formula of feature tree) ∧ (cross-tree constraints)

4. FMs are context-sensitive grammars

   • FDs are context-free language
   • Cross-tree constraints provide context-sensitivity
   • Language = A set of products in a product line
   • Sentence = A particular product
   • SAT solver to analyze propositional formulas

5. SAT Solver

   • Input to a SAT solver is a predicate in conjunctive-normal form (CNF)
   • Janota’s Algorithm for propagating constraints
   • Produce explanations in a SAT solver (BCP + SAT Solver)
   • Check Specification Complete (True, False, Unknown)
   • Debugging

6. Edits (changes) on a feature model:

   • refactoring - if the set of products has not been changed
   • generalization - if the set of products has been enlarged
   • specialization - if the set of products has been shrunk

7. Let F and G be feature models, where edits to F have produced G. Let L(F) and L(G) denote their respective set of products

   • L(F) ⊂ L(G) - G is a generalization of F
   • L(G) ⊂ L(F) - G is a specialization of F
   • L(F) = L(G) - G is refactoring of F Subset relation could be translate to : (L(F) ⊆ L(G)) ≡ (P(F) ==> P(G)). Checking whether P(F) ==> P(G) is a tautology, we use its negation that ¬(P(F) ==> P(G)) = ¬(¬P(F) ∨ P(G)) = P(F) ∧ ¬P(G)
   • Solving this problem is PSPACE-Complete (Similar to NP-Hard)

8. Solution to P(F) ==> P(G) or P(F) ∧ ¬P(G) : When G is produced from F by editing, we would expect G and F to have many clauses in common.

   • P(F) = pF ∧ commonClauses
   • P(G) = pG ∧ commonClauses
   • pG = R1 ∧ R2 ∧ R3 ∧ … ∧ Rn, where each Ri is a disjunction of terms and a term is a feature variable or its negation
   • We can now make n distinct calls to a SAT solver to determine whether (P(F) ∧ ¬ Ri)is satisfiable - which a solver can do efficiently.

9. Use 9 to solve 10:

   • Generalization: P(F) ==> P(G)
   • Specialization: P(G) ==> P(F)
   • Refactoring: P(F) ==> P(G) ∧ P(G) ==> P(F)
   • Limitation: This works if FMs F and G have the same set of concrete features.

10. Feature Addition: ∀ feature A that is in FM G but not in FM F:

    • P’(F) = P(F) ∧ ¬A Feature Deletion: ∀ feature A that is in FM F but not in FM G:
    • P’(G) = P(G) ∧ ¬B
    • Now rerun analysis using P’(F) and P’(G)
    • Limitation: this works for only concrete (terminal) features

11. Non-Terminal Features Solution: replace every abstract feature with its ”definition”

    • Wrong: a non-terminal feature is true iff one of its concrete features is true.
    • Correct: replace each abstract feature with its true predicate definition – may reference other abstract features, so this recurs.
    • No abstract features are shared, only concrete features and reduce to predicates that can be proven equal to a SAT solver.

12. Safe Composition (verifying type safety properties of product lines):

    • We generate one program at a time, and compile it to see if it is type safe
    • We want similar assurances that ALL programs in a SPL are type safe – but how?
    • How can type safety properties of a SPL can be verified by SAT solvers?
    • Light Weight Consistency (No compiler for features)
    • Feature Combinatorics

13. Refinement Constraint:

    • R = F ==> X ∨ Y ∨ Z (Rule or Constraint)
    • FM ∧ ¬R must be satisfied
    • FM ∧ ¬R = FM ∧ F ∧ ¬X ∧ ¬Y ∧ ¬Z

14. Reference Constraint:

    • If features X and Y define m in H1, Sup1(m) = X ∨ Y
    • If features Q and R define n in H2, Sup2(n) = Q ∨ R
    • m is defined is in a product that references m: F ==> Sup1(m) ∨ Sup2(n) ∨ …

15. Single Introduction Constraint:

    • Let m be introduced by features X, Y, Z
    • atmost1(X,Y,Z) = (¬X ∧ ¬Y ∧ ¬Z ) ∨ (X ∧ ¬Y ∧ ¬Z) ∨ (¬X ∧ Y ∧ ¬Z) ∨ (¬X ∧ ¬Y ∧ Z)

Acknowledgement:

This article is my learning notes of course CS392F Automated Software Design, lectured by Prof. Don Batory. The core idea of this course is how to write programs to generate other programs in a scientific way, that is, not by hacking.