Research On Model Transformation And Consistency Verification Of Airborne Software Based On MDA

With the updating of avionics system,the complexity and scale of airborne embedded system are increasing continuously,and the system configuration is gradually changing from electromechanical intensive to software intensive,and the functions and codes realized by airborne software are increasing rapidly.In the development process of airborne system and software,the traditional development method based on code becomes more and more difficult to meet the requirements of rapid development and component reuse.Model Driven Architecture(MDA)can effectively solve the above problems,realize the collaborative development of airborne embedded system,and improve the development efficiency.MDA provides a complete Modeling standard and Modeling Language for the System development process.System Modeling Language(Sys ML)can coordinate Modeling of software,hardware and requirements in the System.Through the MDA model transformation framework,the software model in the system model established by semi-formal language Sys ML can be transformed into the formal model,which meets the requirements of high security of airborne software.The main research work of this paper is as follows:(1)Sys ML extension and subset extraction.Firstly,MARTE(Modeling and Analysis of Real-time Embedded System)is used to extend Sys ML to meet the real-time requirements of airborne Embedded System.In order to ensure the security of software functions in the system model built by Sys ML/MARTE,it was transformed into the formal tool Scade Suite for verification.In order to meet the corresponding relationship with the elements of the Scade model,subset extraction was carried out on the Sys ML model,and model transformation was carried out based on the Sys ML subset.(2)Model transformation method based on MDA.Firstly,the Sys ML/MARTE and SCADE models were metamodel modeled by the same metamodel description language respectively to realize the isomorphization of heterogeneous models.On the basis of isomorphization,according to the principle of semantic equivalence,the mapping relationship from Sys ML/ Marte metamodel elements to SCADE metamodel elements is established,and the semantic mapping rules among metamodel are established by ATL language.Finally,TCS language is used to specify the syntactic specification of the metamodel to generate a model file that can be executed by Scade Suite.(3)Case analysis and consistency verification.The controller software of UAV attitude control system is selected as the verification object,which is modeled by Sys ML/MARTE,and then transformed into SCADE model by the established conversion rules.Based on the consistency requirements of DO-178 C,a consistency verification method was proposed to verify the consistency of the conversion results.The verification method was divided into correctness verification and completeness verification.The model test and the coverage analysis of the test process were used to verify that the conversion process met the consistency requirements.