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.
2008 International Conference on Software Engineering Research & Practice. Proceedings of the 2008 International Conference on Software Engineering Research & Practice, SERP 2008 (Las Vegas, Nevada 14-17 July, 2008) p. 349-355