The Method Research On Resource Modeling And Verification Of Real-Time Software Based On Model Transformation

With the widely improvement and application of reliability and security requirements of real-time software in the industrial community,it has been more and more important and increasing unprecedented in the real-time software. Meanwhile, software reliability has also been the key indicator of real-time software. Althogh the traditional Unified Modeling Language (united modeling language,UML) is applied to the software modeling, there are two drawbacks. (1) For UML,it lacks discriptions for time and resource related which require for more complex system behavior,so it is deficient to modeling real-time software; (2) For UML,it lacks accurate definition of formal semantics and can not be formalized verified and analysed for software model, so it is difficult to ensure software reliability and security. For this two points,it si nessesary to make up through UML profile and formal description of software. Modeling and analysis of real time and embedded systems (MARTE) is a UML profile proposed by OMG and it makes up for the lacks of non-function in time and resourse etc. The formal methods such as petri nets, process algebra, timed price automata are formal description language for software.They describe software system through formal mathematical notation to make it more accurate and reliable.Model Driven Architecture (MDA) is a model-centric software development framework. Its nature is meta modeling and model transformation. In this paper, a MDA-based method on resource modeling and model transformation of real-time software is proposed. This method first abstracts MARTE meta-model which contains some resource information and Priced Timed Automata (PTA) meta-model through meta-modeling. Secondly it use ATL model transformation language to transform instance models from MARTE model to PTA model. The transformation is to construct transformation rules for MARTE meta-model and PTA meta-model. Finally, the result is formal verified through formal tool Uppaal Cora. The case shows the feasibility and effectiveness of the method which can improve the reliability of resource modeling of real-time software.The discussion of this paper as follows:(1) How to abstracts MARTE meta-model which contains some resource information and Priced Timed Automata (PTA) meta-model through meta-modeling.(2) How to use ATL model transformation language to transform instance models from MARTE model to PTA model. The transformation is to construct transformation rules for MARTE meta-model and PTA meta-model.(3) How to verify the result formally through formal tool Uppaal Cora.