An Empirical Study of Flight Control System Model Checking Integrated with FMEA

Cyber-Physical Systems (CPS) is a multidimensional complex system that integrates computing, network and physical environment. Flight control system enables the aircraft to interact with the outside world and other components, which is a typical CPS. The Verification of safety has been a research hotspot. Model checking is a formal verification method with a high degree of automation, including three steps: model construction, properties specifications and execution. In general, Properties has been generated based on the subjective experience of the verifier, and there is a lack of a strict process. We focus on the process of establishing specifications using Failure mode and effect analysis (FMEA) And then use our improved method to do the requirement level model checking about the return process and collision prevention based on PX4 flight control system. The results prove that our method makes the model checking logic clearer and has good adaptability.