The capability to dynamically reconfigure in response to change of mode or function, failures, or unanticipatedhazardous conditions is fundamental for many critical systems. The modelling and verification of suchsystems are frequently carried out with product lines and model checking, respectively. At first, the objectivesand related requirements of reconfigurable systems are mapped to a feature model, whereas the units relatedto operational modes are selected in individual configurations. After that, the proposed approach performsautomated transformation of particular models into formal constraints and descriptions for leveraging the analyticalpowers of model checking techniques; the formal verification of completeness, consistency and conflictis carried out with NuSMV model checker. Finally, in circumstances when the counterexample is produced, itsanalysis is performed for the identification of corresponding problems and their resolutions. The applicabilityof the proposed approach is demonstrated through case study of attitude and orbit control system.