The Research On Model Transformation Based On Mde For Real-time System Verification

How to ensure the safety and reliability of real-time systems, in which the correctness of the system depends not only on the logical results of computation but also on the time at which the results are produced, is widely concerned by researehers. The UML is a widely-used standard modeling language, but it is difficulty to be applied for verification directly. The formal methods support formal verification by transfering the system verification problem into a mathematical one. Therefore, the model verification, through the transformation from UML models to formal models, has become the hotspot in the field of software engineering. The UML profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE) has been recently standardized by the OMG for real-time system modeling. The timed automata (TA) is an effective tool for the verification of model checking, which provides a formal method to establish and analyze the behavior of real-time systems.Model-driven engineering (MDE) is a new paradigm in software engineering which treats models as the first class citizens, and implements software by (meta-)modeling and model transforming. The meta-metamodel in MDE provides a common way of bridging those models conforming to the same meta-metamodel. In this paper, we present a MDE-based approach to build bridges between MARTE models and TA models for verification. It consists of three steps: the first step is the metamodeling of TA, which brings TA into meta-metamodel architecture in MDE; the second is defining mapping rules between metamodels of MARTE and TA, and it is implemented by the platform in support of transformation languages; the third is to rewrite TA models into textual inputs of model checking tools for verification.The main contributions of this thesis are as follows: 1. The MDE-based approach to transform MARTE models into TA models for verification ispresented. It focuses on two aspects: the heterogeneous models integration by metamodeling and the model transformation based on metamodels.2. The metamodel of TA is builded for integrating TA into meta-metamodel architecture. It is intended to ensure that the metamodel of TA has the same"root"as MARTE, so they can have the same operation sets.3. The model transformation based on MDE is implemented by defining transformation rules between metamodels. Because most of model checking tools define their own textual input formats, hence there is an additional process bringing models into textual descriptions.