Research On Refinement-based Ada Code Generation Of AADL Models

Safety-critical software is widely used in avionics,spacecraft,weapons and equipment,and rail transportation.Such software has the characteristics of high security,limited resources,and real-time response.Model-driven development methods based on AADL(Architecture Analysis and Design Language)are widely used in the field of safety-critical software.Automatic code generation based on AADL model is an important research content in this field.For safety-critical software,the generated code often runs on various embedded platforms,such as real-time operating systems,hardware platforms,and bus communications.Existing research has mainly included platform-related information in the code generator in a hard-coded or configured manner to generate the code required by the industry.However,the problem with this approach is that there is a large semantic distance between the generated code and the AADL model(Semantics Gap).For example,it was verified on the AADL model that the model satisfies non-functional properties such as schedulability,but because such temporal properties are often related to hardware platforms,and platform-related information is added by the code generator after model analysis,resulting The generated code may not meet the schedulability,and the time nature is not maintained.Therefore,this thesis proposes a refinement-based AADL model Ada code generation method,which first refines the model,obtains the refined model,performs non-functional analysis,and then performs code generation.The main contributions of this article are as follows:Firstly,an AADL model refinement method for safety-critical software is proposed.The method includes a refinement framework,refinement steps,refinement scenarios,and refinement rules.An AADL model refinement process consists of multiple refinement steps.We express a specific refinement step based on the refinement scenario,and the refinement rule is a way of expressing specific refinement.The refinement of the model provides it with more accurate non-functional attribute analysis capabilities,reducing the semantic distance between the model and the generated code.Secondly,the automatic generation method of Ada code for AADL refinement model is given.The method includes two parts: platform independent code generation rules and platform related code generation rules.Automatic code generation can effectively maintain the validated nature of the model and reduce errors caused by manual coding.Finally,MACAADL2 Ada,an AADL model code generation prototype tool based on refinement,is designed and implemented.The method used in this paper is analyzed by the actual case of the industry,namely the satellite attitude orbit control system,and the validity of the method is verified.Tested and simulated to demonstrate correctness of generated code.