  For the verification of systems using model-checking techniques, symbolic
representations based on binary decision diagrams (BDDs) often help to tackle
the well-known state-space explosion problem. Symbolic BDD-based
representations have been also shown to be successful for the analysis of
families of systems that arise, e.g., through configurable parameters or
following the feature-oriented modeling approach. The state space of such
system families face an additional exponential blowup in the number of
parameters or features. It is well known that the order of variables in ordered
BDDs is crucial for the size of the model representation. Especially for
automatically generated models from real-world systems, family models might
even be not constructible due to bad variable orders. In this paper we describe
a technique, called iterative variable reordering, that can enable the
construction of large-scale family models. We exemplify feasibility of our
approach by means of an aircraft velocity control system with redundancy
mechanisms modeled in the input language of the probabilistic model checker
PRISM. We show that standard reordering and dynamic reordering techniques fail
to construct the family model due to memory and time constraints, respectively,
while the new iterative approach succeeds to generate a symbolic family model.
