Airborne Software Modeling And Formal Verification Methodology

With the improvement of reliability requirements and the increase of code complexity of airborne software,the deficiency of traditional software development methods is becoming more and more obvious.Meanwhile,the traditional software verification method of designing and executing test cases can hardly meet the high safety requirements of airborne software.Based on the above background,this thesis adopts model-based method to realize the development of airborne software of a certain type of aircraft,and uses formal verification technology to verify some key safety modules.The specific work is as follows:Firstly,after analyzing the characteristics of airborne code and comparing three formal verification methods,theorem proving is selected as the basic verification method.Aiming at its low degree of automation,a deductive verification system based on Hoare logic and the weakest prepredicate calculus is adopted to help the automatic extraction of verification conditions(VC),and combined with relevant tools for analysis and selection,a formal verification scheme for airborne code is designed.Then in order to further enhance the automation of verification,in the building of Hoare logic code is studied based on the ACSL implementation method and extraction method on the basis of the verification condition,combining auto-active proof idea,puts forward a method to build a code supplement-through the ACSL build auxiliary lemma and auxiliary assertions,and,when necessary,use Ghost code will lemma instantiation,make can generate more can be released automatically proof of verification of the condition,thus improve the degree of automation and efficiency of formal verification.At the same time,in order to meet the requirements of high security of airborne software,the security protocols for formalizing three kinds of threats to airborne software,such as arithmetic overflow,are summarized.Finally,based on the actual engineering project of an aircraft design institute,the model-based software development method is used to model the flight control airborne software of a certain type of unmanned aerial vehicle and generate the airborne code.Taking this as the verification object,the aircraft front wheel steering circuit management module,total pressure sensor monitoring module and attitude resolution module in the project as examples,the validation method proposed in this thesis is usedfor formal verification,which proves the effectiveness and feasibility of this method.The closed loop simulation is carried out on the virtual flight control simulation platform,and the experimental results show that the airborne software developed in this thesis conforms to the performance indexes.The research of this thesis provides a reference for the development of formal verification in airborne software and other fields with high security.