Behavioral Fault Modeling And Formal Verification Method Of Aviation Control System Using BIP

In recent years,our country’s aviation industry has developed rapidly,and people use civil aviation aircraft more and more frequently in their daily production and life.From commercial passenger planes,cargo planes and dual-purpose planes,to generalpurpose agricultural machines,forestry machines,patrol air ambulances,feeder transport aircraft,etc.While these civil aviation aircrafts bring convenience to people’s lives,they are also accompanied by risks.Once the hardware and software system fails,it can cause damage to the user’s property,and cause casualties in the worst case.Therefore,safety and reliability are what aviation engineers need to focus on when designing and developing civil aviation aircraft.Formal method is a method based on mathematical theory to ensure the safety and reliability of the system design,development and verification process.By using formal methods,engineers can provide formal specifications for requirements,establish abstract formal models for systems,and provide formal verifications for system models,thereby improving the security and reliability of the target system.Therefore,it is feasible to use formal methods to provide modeling and verification support for the control system in the aviation field,and it is also the mainstream trend and vision.On the other hand,as a standard for ensuring safety and reliability when developing civil aviation aircraft,the Aerospace Information Report 6110(AIR 6110)issued by SAE International introduces guidelines and methods for the safety assessment process of civil airborne systems and equipment.AIR6110 provides guiding principles for the safety assessment process of the aviation control system architecture.Through the results of the safety assessment,it guides the design of the architecture,and finally obtains the aviation control system architecture that meets the safety requirements.However,the practical application of this standard in the industrial field is difficult for two reasons:(1)AIR6110 did not specify the specific technology used in the safety assessment process,and the lack of accurate normal and fault models at the system architecture level makes the current mainstream means of implementing AIR6110 still manual and informal methods.Engineers need to put a lot of effort into manual system modeling and safety evaluation makes the safety evaluation process highly dependent on the engineer’s ability and experience.The results are subjective,costly,and quality cannot be guaranteed.(2)The separation of the system model and the fault model makes the fault information that the security engineer pays attention to cannot be reflected in the system model.Some deep faults generated by the interaction between components due to the architectural design are easily ignored.In response to the above problems,this paper proposes a behavioral fault modeling and verification technology for aviation control systems based on formal methods.We use formal methods to establish a system model for the system at the architecture design level,and generate a fault model through system fault behavior,and combine the two into a unified extended system model.By applying formal verification methods to the extended model,we can ensure the necessary safety attributes in the design at the earliest design stage,and gradually refine the specific details of the model.We took the civil aircraft wheel brake system introduced in AIR6110 as the research object,and verified that our method can provide automated support for the safety evaluation process in the field of aviation control systems,reducing costs and improving the efficiency and quality of safety evaluation.The main work of this paper includes the following aspects:· Behavioral fault modeling method based on Behavior Interaction Priority(BIP)A BIP-based behavioral fault modeling method at the system architecture level is proposed.In the field of specific aviation control systems,different from the traditional modeling method that separates the informal system model and the fault model,the method we propose can be based on the BIP language to establish a unified formal fault that includes architecture and fault behavior information Model.· Formal verification of BIP fault model The formal fault model is verified by a statistical model checking method based on simulation execution.At the aviation control system architecture level,different from the traditional manual inspection method,the statistical model inspection method based on simulation execution applied in the formal failure model can effectively improve the efficiency of safety assessment and guide the iterative process of the architecture.· Extension of SBIP Model Checking Tool The model checking tool SBIP has been extended in terms of automated fault modeling.On the basis of the SBIP tool,a plug-in that supports the fault component generation and fault injection functions in the fault model generation process introduced in this article is implemented.