Modern automotive systems are composed of hundreds of software-implemented features often interacting with physical subsystems under real-time constraints. For efficient management of their development, the features are conceived and realized as product lines involving variability with different variants being deployed in different vehicle classes. The variability information is expressed at different levels of abstraction during the various phases of development, like requirements, design and implementation. We introduce and study a formal model of such feature product lines capable of capturing variability and real-time behavior. We define a notion of conformance to relate the variability at different levels of abstraction and propose a compositional method of verifying conformance of multiple features. The proposed approach naturally extends to hybrid system behaviors consisting of discrete and continuous plant variables. We demonstrate the applicability of the approach by giving a simple paradigmatic example.

In a Software Product Line (SPL), the central notion of implementability provides the requisite connection between specifications (feature sets) and their implementations (component sets), leading to the definition of products. While it appears to be a simple extension (to sets) of the trace-ability relation between components and features, it actually involves several subtle issues which are overlooked in the definitions in existing literature. In this paper, we give a precise and formal definition of implementability over a fairly expressive traceability relation to solve these issues. The consequent definition of products in the given SPL naturally entails a set of useful analysis problems that are either refinements of known problems, or are completely novel. We also propose a new approach to solve these analysis problems by encoding them as Quantified Boolean Formula(QBF) and solving them through Quantified Satisfiability (QSAT) solvers. The methodology scales much better than the SAT-based solutions hinted in the literature and is demonstrated through a prototype tool called SPLANE (SPL Analysis Engine), on a couple of fairly large case studies.