The Conversion Research From AADL To UPPAAL And Tool Integration

With the advancing of modernization and the development of communication technology, computer software has been widely applied in various real time critical systems. As the complexity in the designing of real time critical system escalates, it is impossible to fullfill the growing requirement of complex system designing with the traditional software engineering method. Currently, by combining the development method MDA (Model Driven Architecture) and AADL (Architecture Analysis and Design Language),developers have achieved a good effect in such systems. However,the tool chain of AADL is somewhat insufficient in analogy and simulation of the system. To solve this problem, this paper studies relavant research and proposes a practicable method.In this paper,main works are listed as follows.Firstly,this paper designs a set of conversion rules from AADL model to timed automata network UPPAAL (UPPSALA University and AALBORG University)model. This paper designs a subset of AADL from the AADL complete set according to a set of specific principle including minimization principle,descriptive principle and realization principle. Based on this subset which fullfills the requirements of designing real time critical system, this paper designs and implements the conversion rules from AADL model to UPPAAL model. By converting the model,we can use rich tools and resources of timed automata network to analyze AADL model.Secondly, this paper designs a set of conversion rules from behavior annex of AADL model to timed automata network UPPAAL model. This paper designs a subset of AADL behavior annex from the AADL behavior annex complete set according to a set of specific principle including minimization principle, descriptive principle and realization principle. Based on this subset which fullfills the requirements of designing real time critical system, this paper designs and implements the conversion rule from AADL behavior annex model to UPPAAL model.Thirdly, to reduce the complexity in the designing of transformation rules from AADL model to timed automata model, this paper proposes and implements a rule generator to generate ATL (Atlas Transformation Language) rules from existing UPPAAL templates.Fourthly,a conversion system including all the designment in this paper is implemented based on Eclipse Plug-In and XMI.At last, two pratical cases are analysed on the system implemented by this paper.In summary, the method proposed and the conversion system implemented in this paper is capable of transforming and verifying the designed model in the MDA method,and has a good effect in the development of real time critical systems.