Software product line engineering deals with the combined development of a family of similar software systems. These systems provide a similar set of features and should therefore share a large number of common components. We study the user perspective of features and the engineering perspective of components and present a formal notion of features, component-based product families and their interaction. We then demonstrate using Milner's CCS how our formalism can be applied to extend an arbitrary modelling formalism with support for product lines. To verify that certain products indeed realize certain features, we propose μ-calculus model-checking for multi-valued Kripke-structures. The model checking result in that case no longer is a simple truth-value, but a set of products, conforming to a certain property.

Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change
EditorsTiziana Margaria, Bernhard Steffen
Number of pages15
Volume7609 LNCS
Place of PublicationBerlin
PublisherSpringer Verlag
Publication date07.11.2012
Edition PART 1
ISBN (Print)978-3-642-34025-3
ISBN (Electronic)978-3-642-34026-0
Publication statusPublished - 07.11.2012
Event5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Technologies for Mastering Change
- Heraklion, Crete, Greece
Duration: 15.10.201218.10.2012
Conference number: 93454


Dive into the research topics of 'A Formal Approach to Software Product Families'. Together they form a unique fingerprint.

Cite this