Formal definition of feature models to support software product line evolutions

Feature models have been widely used in software product line based software engineering. The dependencies between the variants and variation points in a feature model have very strong implications on the product configurations. Usually these dependencies are represented informally and incomplete in existing feature modelling approaches. In this work we first further explore the complex dependencies existing in software product lines. And then we propose a formal specification using Z notation to specify the dependencies in a product line. The specification formally defines software product lines and specifies complex dependency constrains contained in product lines. A set of operation schemas that support product line evolutions have been developed. With these operation schemas the invariants defined in the formal specification of product lines can be ensured when new features and feature dependencies are added into or removed from the product line. As Z specifications provide proof mechanism to validate the formal model and natural transition from a specification to an implementation a reasoning mechanism and a feature modelling tool can be developed in future.