https://www.mdu.se/

The capability to dynamically reconfigure in response to change of mode or function, failures, or unanticipated hazardous conditions is fundamental for many critical systems. The modelling and verification of such systems are frequently carried out with product lines and model checking, respectively. At first, the objectives and related requirements of reconfigurable systems are mapped to a feature model, whereas the units related to operational modes are selected in individual configurations. After that, the proposed approach performs automated transformation of particular models into formal constraints and descriptions for leveraging the analytical powers of model checking techniques: the formal verification of completeness, consistency and conflict is carried out with NuSMV model checker. Finally, in circumstances when the counterexample is produced, its analysis is performed for the identification of corresponding problems and their resolutions. The applicability of the proposed approach is demonstrated through case study of attitude and orbit control system.