  This paper presents our approach to the quantitative modeling and analysis of
highly (re)configurable systems, such as software product lines. Different
combinations of the optional features of such a system give rise to
combinatorially many individual system variants. We use a formal modeling
language that allows us to model systems with probabilistic behavior, possibly
subject to quantitative feature constraints, and able to dynamically install,
remove or replace features. More precisely, our models are defined in the
probabilistic feature-oriented language QFLAN, a rich domain specific language
(DSL) for systems with variability defined in terms of features. QFLAN
specifications are automatically encoded in terms of a process algebra whose
operational behavior interacts with a store of constraints, and hence allows to
separate system configuration from system behavior. The resulting probabilistic
configurations and behavior converge seamlessly in a semantics based on
discrete-time Markov chains, thus enabling quantitative analysis. Our analysis
is based on statistical model checking techniques, which allow us to scale to
larger models with respect to precise probabilistic analysis techniques. The
analyses we can conduct range from the likelihood of specific behavior to the
expected average cost, in terms of feature attributes, of specific system
variants. Our approach is supported by a novel Eclipse-based tool which
includes state-of-the-art DSL utilities for QFLAN based on the Xtext framework
as well as analysis plug-ins to seamlessly run statistical model checking
analyses. We provide a number of case studies that have driven and validated
the development of our framework.
