Design-Time Verification of Reconfigurable Real-time Embedded Systems

In this paper, we propose a framework allowing the modeling and verification of reconfigurable Distributed Real-time Embedded (DRE) systems. In fact, as reconfiguration significantly complicates system design and execution, many non-functional properties and constraints cannot be easily preserved. Verifying the continuous satisfaction of non-functional properties should be thus accomplished after applying reconfiguration actions. For this purpose, we develop an integrated model-based development approach allowing modeling and verification of reconfigurable DRE systems.