Timing Assurance of Avionic Reconfiguration Schemes Using Formal Analysis

Reconfigurable avionics systems can tolerate faults by moving functionalities from failed components to another available system component. This paper proposes a distributed reconfigurable architecture for application migration from failed modules to working ones. The feasible system reconfiguration states are determined off-line to provide the expected configuration in foreseen situations. Model checking is used to determine feasible configurations evaluating specific temporal properties. A case study is used to show the application of the presented approach as a proof of concept.