  Parametric model checking (PMC) computes algebraic formulae that express key
non-functional properties of a system (reliability, performance, etc.) as
rational functions of the system and environment parameters. In software
engineering, PMC formulae can be used during design, e.g., to analyse the
sensitivity of different system architectures to parametric variability, or to
find optimal system configurations. They can also be used at runtime, e.g., to
check if non-functional requirements are still satisfied after environmental
changes, or to select new configurations after such changes. However, current
PMC techniques do not scale well to systems with complex behaviour and more
than a few parameters. Our paper introduces a fast PMC (fPMC) approach that
overcomes this limitation, extending the applicability of PMC to a broader
class of systems than previously possible. To this end, fPMC partitions the
Markov models that PMC operates with into \emph{fragments} whose reachability
properties are analysed independently, and obtains PMC reachability formulae by
combining the results of these fragment analyses. To demonstrate the
effectiveness of fPMC, we show how our fPMC tool can analyse three systems
(taken from the research literature, and belonging to different application
domains) with which current PMC techniques and tools struggle.
