Analytical Software Design (ASD) enables model-based development of
component software systems. Until now, functional verification of ASD
systems is only possible on a per-component basis. There is no
functional verification engine for ASD itself, so this verification
relies on a translation of individual components to mCRL2, a
process-algebraic model checker. We show how to extend the ASD-mCRL2
translation to support multiple components in order to enable checking
of system wide functional properties. With our extended translation, we
perform a case-study on a newly developed industrial system consisting
of 26 communicating components. The results indicate that it is feasible
to model check functional properties on this scale.