Formal Verification and Automated analysis of Software Product Lines

Software Product Line Engineering (SPLE) is a software development paradigm supporting the joint design of closely-related software products in an efficient and cost-effective manner. The starting point of a Software Product Line (SPL) is the scope, which defines all of the possible features of the products in the SPL. The scope is said to define the problem space of the SPL, describing the expectations and objectives of the product line. The description is typically organized as a feature model [1] that expresses the variability of the SPL in terms of relations or constraints (exclusion, requires dependency) between the features and defines all of the possible products in the product line.
An important step in SPLE is the development of core assets, a collection of reusable artifacts. The core assets contains the components, and we use the term component to represent any artifacts that contribute to product development, like code, design, documents, test plan, hardware, etc. A component is an abstract concept of any assets used in products.