A Framework for Simulation and Formal Verification of Redundant Flight Control Systems with Components Subject to Partially Synchronous Timing Effects

---In this paper we propose a simulation framework where the effects of timing on the application layer can be reproduced. The framework supports both simulation-based testcase generation and formal verification methods. It is centered around a timing model that is representative to real-time flight control systems. This timing model is also presented in this work along with several observations that are a result of the temporal behavior of the model. Simulation results demonstrate that the observations can be reproduced with the framework. It can be used as a tool to prove the correctness of the functional design of flight control application layers that need to be robust against such effects.     «

---In this paper we propose a simulation framework where the effects of timing on the application layer can be reproduced. The framework supports both simulation-based testcase generation and formal verification methods. It is centered around a timing model that is representative to real-time flight control systems. This timing model is also presented in this work along with several observations that are a result of the temporal behavior of the model. Simulation results demonstrate that the obse...     »