Formal Verification Research Of Driver Module Based On Small UAV Flight System

Since the small unmanned aerial vehicle was invented,it has been receiving widely attention from all fields of the society,and its development history in last several decades has greatly proved that it has infinite potential.The small UAV seems to become a part of people's life.However,with its increasingly wide application,its security has become increasingly prominent,and it undoubtedly brings a certain threat to personal security and property.Therefore,the security problem of UAV must be paid attention to and improved.Focus on the safety and reliability of a computer system,there is a new advanced technology named “System Safety and Reliability's Verification”.In 2015,the Flint laboratory in Department of Computer Science comes from Yale University in United State,posted a new small kernel named CertiKOS(Certified Kit Operating System),and in the meanwhile indicated that its implementation modules had all been verified.This process has greatly improved the problem that there might be some unknown errors or bugs in the system.In other to improve the safety and reliability of UAV system from its software level,this dissertation re-designs and re-implements the driver module in the lower layer and attitude fusion module in the high layer of the small UAV system.Aim at the driver module,this dissertation innovatively posts that make advantage of the advanced technology of system software verification,to verify the safety and reliability of the driver module in UAV system,and to improve the problem that there might be some unknown errors and bugs in the UAV system from its driver layer,so as to improve the safety and reliability of UAV flight system.Aim at the attitude fusion module,this dissertation uses the gradient method of optimization algorithm,compared with the traditional attitude fusion module based on Calman filter,it has the same performance but with simple implementation,less computation,and better reduces the computation of CPU.Finally,this dissertation combines the safety-and-reliability-verified modules and the safety-and-reliability-unverified modules to construct a compositional verification UAV flight system,and applies it into the real physical system of the UAV platform.The related experimental result shows that the safety-and-reliability-verified modules can be well applied to the real system,and improved the problem that there might be some unknown errors or bugs in the driver of the UAV flight system.And of course,to improve the safety and reliability of the UAV system.On improving the safety and reliability of UAV system,the research in this dissertation is of great significance.