Research On Formal Verification Of Airborne Software Safety

The modern planes as a kind of vehicles working in the air require high security,any minor mistakes could cause disastrous consequences.So,aircraft safety is very important.The various functions of the modern airplanes are increasingly dependent on software system.However,modern airborne software has various functions,complex structures and numerous components,which are affected by many factors,especially the influence of components depend on each other on design phase cannot be completely ruled out,resulting in a decline in the overall situation of security situation.To ensure the safety of the software,developers need to ensure the security requirements in the design phase.However,the present method is difficult to meet the requirement of security validation.Thus,an efficient system components security validation method is necessitated to ensure the system safety design to meet the airworthiness standards requirements.Using SysML language can better describe the airborne software architecture and features,but SysML is a half-formalized tool,lack of precise semantics support and doesn't have the validation at the same time.Petri net is formal tools.It has graphical features and precise semantic features,and has been widely applied in the field of formal verification.Through the proper way to convert SYSML into Petri net model,it's convenient to further verify the software security.So that developers can find out the deficiency in the design of the software,to avoid the rework and to find potential safety hazard,eventually ensure the security of the system.This thesis firstly searches the airworthiness rules of airborne software and on this basic definition the Petri nets suited to describe the problem of airborne software safety consistency verification.Then this thesis build a static structure model,including safety attributes of system based on the SysML block diagram and build rules to translate SysML block diagrams to Petri nets in order to build formal model accurately.Accordingly,this thesis uses reachability tree to analyze all delivery paths of safety relations and all combinations of safety states of the system,on basic of which,giving the safety verification algorithms to ensure whether the design of software architecture and combinations of components' safety levels meet the airworthiness criterion DO-178 C.Finally,this thesis confirms this method's feasibility by one example and analyzes advantages of the method based on Petri nets in software safety verification by comparing with other methods.