Dissertation > Excellent graduate degree dissertation topics show
The Research on Model Transformation Based on MDE for Real-Time System Verification
Author: LiuYaPing
Tutor: HuangZhiQiu
School: Nanjing University of Aeronautics and Astronautics
Course: Applied Computer Technology
Keywords: model-driven engineering model verification model transformation MARTE timed automata
CLC: TP311.52
Type: Master's thesis
Year: 2009
Downloads: 60
Quote: 1
Read: Download Dissertation
Abstract
|
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.
|
Related Dissertations
- Service Model Driven Architecture (SMDA) Oriented Modeling Techniques and Tool Implemention,TP311.52
- Research on Traceability and Incremental Consistency of the MDA Model Transformation,TP311.5
- The Research on Transformation from PIM to PSM for Seam,TP311.52
- High-speed train multibody dynamics parameter extraction and model transformation key technology research,TP391.72
- A Study on Statecharts Modeling Framework Based on SMP2,TP391.1
- Formal Verification of Safety Computer Platform in CBTC System Based on Timed Automata Model,U284.48
- Advanced Vocational Education in Fujian Talent Cultivation Model Transformation in Researching,G718.5
- Research and Implementation of the Heterogeneous Target Platform-Oriented MDA,TP311.52
- MDA-Based Transforation between UML Models,TP311.52
- Research and Implementation of Data Model Transformations Based on XSLT,TP311.52
- Research on UML Model Transformatin Based on MDA,TP311.52
- Research on Model Transformation Technology of Internetware,TP311.52
- The Research of Transformation in Local Teachers Colleges,G652.4
- Control Design for Magnetic Levitation Systems,TP273
- A Model-Driven Approach for Dynamic Web Service Composition,TP393.09
- Flexible workflow process model,TP311.52
- IF graphical models of real-time software design verification,TP311.52
- Research on Transformation from Use Case Diagrams to Sequence Diagrams,TP311.52
- Design and Implementation of Model Transformation Tool Based on MDA,TP311.52
- MDA-based software development model research and application,TP311.52
CLC: > Industrial Technology > Automation technology,computer technology > Computing technology,computer technology > Computer software > Program design,software engineering > Software Engineering > Software Development
© 2012 www.DissertationTopic.Net Mobile
|