Abstract
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 language | English |
---|---|
Title of host publication | Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change |
Editors | Tiziana Margaria, Bernhard Steffen |
Number of pages | 15 |
Volume | 7609 LNCS |
Place of Publication | Berlin |
Publisher | Springer Verlag |
Publication date | 07.11.2012 |
Edition | PART 1 |
Pages | 131-145 |
ISBN (Print) | 978-3-642-34025-3 |
ISBN (Electronic) | 978-3-642-34026-0 |
DOIs | |
Publication status | Published - 07.11.2012 |
Event | 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Technologies for Mastering Change - Heraklion, Crete, Greece Duration: 15.10.2012 → 18.10.2012 Conference number: 93454 |