Model-Based UAV Flight Control System Modeling And Safty Verification Methodology

UAV flight control system as one of the key aircraft system is responsible for the entire flight process of the aircraft from taking-off to landing.The flight control system software has the characteristics of safety-critical performance,multifunction and high complexity.However there are many deficiencies in traditional software development methods.At the same time,the formal verification method is used to verify the safety of the flight control system software.There is no unified and effective method to extract the safety properties.The validation of the safety properties is prone to the space explosion problem.How to reduce the state space is also an important task in the current situation.In this thesis,the software development tool SCADE is used to develop the flight control system software.At the same time,the safety property extraction method based on the fault tree is studied in view of the safety-critical and reliability requirements of the flight control system software.The safety verification is carried out in combination with the model checking.In order to solve the space explosion in the process of verification,this thesis proposes a method of segmenting and verifying the verification space based on the slicing and system decomposition.This thesis mainly includes the following aspects:Firstly,we study safety property extraction method and model checking technique.This thesis introduces the model of software development based on model,and puts forward the construction criteria of specific fault tree and the method of safety property extraction and transformation.Secondly,the problem of state space reduction is studied.In order to solve the problem of state space explosion during formal verification,the state space is reduced by using slicing and system decomposition methods.Finally,we carry out flight control system modeling and formal verification of typical modules.We analyze the requirements of the flight control system software,divide and model functional modules.The safety properties are extracted and verified for the typical modules.The code generated from the models is loaded into the emulation testing platform to verify its functionality and performance,and compares it with the manual code.The research of this thesis has a certain effect on the software development,safety property extraction,state space reduction and formal verification of flight control system software,which provides some help for other model-based development and verification workers.