In this paper, we propose a multi-scale modeling methodology for software reconfigurable systems using the formal technique of Bigraphical Reactive Systems. This methodology provides a correct by design approach for the description of multi-scale architectures. It is based on a rule-oriented refinement process ensuring the transitions between scales. In fact, a first scale is defined by the designer. Then, it is refined by successively adding lower scale details. The applied rules respect the system constraints ensuring the correctness of the obtained scale architectures. Furthermore, we deal with the dynamic aspect of multi-scale systems by providing model-based rules of reconfigurations. We illustrate our approach with a Smart Buildings case study.

This paper proposes a verification approach of reconfigurable Distributed Real-time Embedded (DRE) systems. Since dynamic reconfiguration significantly complicates the execution of such a system, it is necessary to ensure the preservation of non-functional properties after applying a such reconfiguration. The proposed approach allows thus verifying non-functional properties at design time. Using our verification approach, the designer can easily verify these properties without deep knowledge of existing verification techniques.