| The avionics system is a safety-critical system with extremely high reliability requirements,and formal verification will run through each life cycle stage of the avionics system.In industry,EA is widely used in model building in various fields due to its universality.In the field of avionics,AADL is widely used due to its excellent aviation architecture capabilities.How to improve the formal verification capability of EA and the architecture analysis capability of avionics system is a problem to be solved.According to the characteristics and requirements of the avionics system,the tool chain proposed in this paper is a type of model converter,including SafetySysML and EA2 AADL,which aims to convert the SafetySysML model into an EA model and then into an AADL model.The main contributions of this paper include:Research methods of model transfer between different platforms.By studying and formulating the model constraint files of each platform,the interface or class file of the model is generated.Then,a series of model mapping sets are formulated to realize the function of model conversion between different platforms.Designed and implemented the SafetySysML2 EA model conversion tool.SafetySysML2 EA takes SafetySysML as the main formal modeling language,takes the safety automatic state machine as the carrier,and takesMDA as the main theoretical basis to convert the safety automatic state machine model after successful verification to the EA model.Integrate the SafetySysML2 EA conversion tool with the S2 M verification chain.In the process of model transformation,this paper integrates the S2 M model verifier to realize the security verification of the state machine.According to different verification purposes and sequences,this paper proposes a method of command chain for verification.Design and implement EA2 AADL model conversion tool.EA2 AADL is a model conversion tool that takes the SysML block diagram(BDD/IBD)and state diagram on the EA platform as input and takes the AADL model as the output,aiming to convert the EA model into an AADL model.Its transformation idea and logic are similar to the SafetySysML2 EA tool.In order to demonstrate the correctness of the transformation tools,this paper takes the aircraft guidance system as an example to illustrate the specific application of the SafetySysML2 EA and EA2 AADL model transformation tools in the avionics system. |