Research On Airborne Safety Critical Software Model Verication Technology

Modern electronic airborne systems are changing from electromechanical-intensive to software-intensive,and the realization of system functions is increasingly dependent on software,resulting in the security of software being critical to the security of the system.Software testing is a method used to verify the correctness of software functions during development.However,the safe operation of safety-critical systems cannot be guaranteed by the correctness of software functions.The software must be validated against the security requirements identified by the security analysis and needs to identify unexpected functions to ensure that the identified potentially dangerous behaviors do not occur.The complexity of software makes it difficult to define appropriate software security requirements using traditional security analysis methods.System Theoretic Process Analysis(STPA)is a security analysis method based on Systems Theoretic Accident Model and Processes(STAMP),used to identify system hazards,including software-related hazards However,this method relies heavily on analyst experience.In addition,there is a trend to adopt model-based software development methods in actual engineering.To this end,this thesis takes the model as the core,and an airborne software model verification method based on the combination of formal extended STPA method and RTCA DO-331 airworthiness standard was proposed.The main research work and innovations of this thesis were as follows:(1)This thesis first uses the Safety Critical Application Development Environment(SCADE)to develop drone flight control system software to ensure the ambiguous nature of the software,and at the same time to build a drone mathematical model based on the drone aerodynamics,To realize the functional simulation of the flight control system and complete the software function verification.(2)In order to improve the security of the software,this thesis proposes a method based on the formal extension of the STPA method to capture software security requirements and form formal specifications,combined with model checking technology to verify the software security.This method starts from system specifications,determines system-level accidents and dangers that may result from system software failure,builds a software security control structure,and identifies dangerous behaviors in the software.Based on the identified potentially dangerous behaviors,combined with the built software process model for further detailed analysis,determine the cause of each potentially dangerous behavior,and translate it into corresponding software security requirements,and then form a protocol model.With the help of model inspection technology,Complete software security verification.(3)In the field of airborne electronic equipment,in order to ensure the software security of airborne electronic equipment,compliance verification is required based on airworthiness standards of airborne software.In order to further improve the safety of safety-critical software,this thesis validates the airworthiness targets such as model coverage and code coverage in RTCA DO-331 using a requirements-based test coverage method to ensure that safety-critical software does not perform functions other than expected.