学位论文 > 优秀研究生学位论文题录展示

基于MDE的UML模型到形式化模型的转换方法研究

作　者: 刘亚萍
导　师: 黄志球
学　校: 南京航空航天大学
专　业: 计算机应用技术
关键词: 模型驱动工程 模型验证 模型转换 UML/MARTE 时间自动机
分类号: TP311.52
类　型: 硕士论文
年　份: 2009年
下　载: 60次
引　用: 1次
阅　读: 论文下载
 

内容摘要


实时系统的正确性不仅取决于计算的逻辑结果,而且依赖于系统运行的时间。如何确保实时系统的正确性和可靠性是软件研究人员广泛关注的问题。UML (united modeling language)是一种通用的标准化的建模语言,适用于软件开发的各个阶段,但其缺乏精确的语义信息,因此难以直接进行验证。而形式化方法(formal methods)提供了一种严格精确的数学方法,通常被用于软件设计阶段,分析系统的可靠性。因此,通过将UML模型转换到形式化模型进行模型验证,是保证软件质量的有效手段。MARTE (modeling and analysis of real time and embedded systems)是OMG组织专门针对嵌入式实时系统的建模规范,用于取代原有的UML-SPT (uml profile for schedulability, performance and time)。时间自动机(the timed automata)是一种成熟的实时系统模型验证工具,它扩展了自动机理论,并为实时系统行为的创建和分析提供了一种形式化方法。模型驱动工程(model-driven engineering,简称MDE)的理念伴随着人们对软件系统的不断抽象,而逐渐受到重视。它以模型为首要软件制品(software artifact),其主要的研究方向为(元)建模和模型转换。元-元模型体系(meta-metamodel architecture)根据抽象度的不同,划分出元-元模型(meta-metamodel)、元模型、模型(和实例)等三(四)个层次,其中抽象度低的模型遵从抽象度高的元模型。元-元模型是元模型的“根”,它为所有遵从它的元模型之间的桥接,提供了一种共同的方式。本文给出了一种基于MDE的UML/MARTE模型到时间自动机模型的转换方法,它包含三个步骤:首先通过时间自动机的元建模,将其引入到MDE的元-元模型体系中;然后,定义UML/MARTE和时间自动机元模型之间的映射规则,并由模型转换语言的支撑平台实施转换过程;最后,按照模型检测工具的输入格式,将转换得到的时间自动机模型进行重写,以便进行模型验证。本文先后探讨了:1.如何基于MDE,将UML/MARTE模型转换到时间自动机验证模型。它关注两个方面:1)如何将时间自动机集成到元-元模型体系;2)如何实现基于元模型的模型转换。2.通过对时间自动机元建模,将其集成到元-元模型体系。集成的目的是为了让时间自动机和UML/MARTE拥有共同的“根”和操作集,从元模型层实现两者的相互理解。3.通过定义元模型层的映射规则,实现UML/MARTE模型到时间自动机模型的转换。转换过程实际上是由映射规则定义语言的支持平台执行。由于模型检测工具通常由自己的输入格式,因此,整个模型转换过程还附带了从模型到文本描述转换的过程。

全文目录


摘要  4-5
Abstract  5-10
第一章 绪论  10-14
  1.1 课题研究背景  10-11
  1.2 研究现状及选题依据  11-13
    1.2.1 国内外研究现状  11-12
    1.2.2 选题依据  12-13
  1.3 论文主要工作及组织结构  13-14
第二章 基于MDE 的模型转换框架  14-24
  2.1 模型驱动工程(MDE)  14-18
    2.1.1 模型驱动体系结构  15-16
    2.1.2 领域特定语言  16-17
    2.1.3 MDE 实现平台和工具  17-18
  2.2 模型和模型转换  18-21
    2.2.1 模型与元模型  18-19
    2.2.2 纵向模型转换  19-20
    2.2.3 横向模型转换  20-21
  2.3 面向验证的模型转换方法  21-23
    2.3.1 模型转换过程  21-22
    2.3.2 模型转换实现途径  22-23
  2.4 本章小结  23-24
第三章 实时系统建模语言的元模型  24-37
  3.1 UML 实时扩展(MARTE)的元模型  24-27
    3.1.1 时间相关的建模元素  25-26
    3.1.2 系统设计建模元素  26-27
  3.2 时间自动机的元模型  27-31
    3.2.1 时间自动机的语法和语义  27-29
    3.2.2 时间自动机的类型结构  29-31
  3.3 MARTE 和时间自动机元模型间的同构化  31-36
    3.3.1 同构化的实现方法  31-32
    3.3.2 与MARTE 同构的时间自动机元模型  32-36
  3.4 本章小结  36-37
第四章 MARTE 模型到时间自动机模型的转换  37-49
  4.1 模型转换的内容  37-39
    4.1.1 模型转换的实施原理  37-39
    4.1.2 模型转换实施过程  39
  4.2 元模型间的映射关系  39-45
    4.2.1 类型结构的映射规则  40-41
    4.2.2 行为的映射规则  41-45
  4.3 模型到文本的相互转换  45-47
    4.3.1 模型到文本的转换  45-47
    4.3.2 文本到模型的转换  47
  4.4 本章小结  47-49
第五章 模型转换的应用  49-61
  5.1 实时系统问题描述  49
  5.2 采用MARTE 的系统建模  49-51
  5.3 MARTE 到时间自动机的模型转换  51-56
  5.4 验证的输入模型生成  56-58
  5.5 模型检测与分析  58-60
    5.5.1 模型检测  58-59
    5.5.2 检测结果分析与讨论  59-60
  5.6 本章小结  60-61
第六章 总结与展望  61-63
  6.1 论文总结  61-62
  6.2 今后工作  62-63
参考文献  63-67
致谢  67-68
在学期间的研究成果及发表的学术论文  68

相似论文

  1. 面向SMDA的服务建模方法及工具实现,TP311.52
  2. 仿真系统模型验证方法和工具研究,TP391.9
  3. 基于时间自动机模型的CBTC系统安全计算机平台的形式化验证,U284.48
  4. 基于时间自动机的模型验证技术,TP301.1
  5. IF对实时软件设计图形模型的验证,TP311.52
  6. 分布式实时系统调度分析工具的改进研究,TP311.52
  7. 基于时间自动机的CTCS-3级列控车载设备建模与验证,U284.48
  8. 基于XYZ/ADL的Web服务组合验证研究,TP393.09
  9. 基于OOTCPN模型的嵌入式系统设计方法研究,TP368.1
  10. 基于时间自动机的可生存性评估方法研究,TP393.08
  11. 基于时间自动机的RBC控车流程研究,U284.48
  12. 一种针对基于构件的嵌入式实时软件的测试方法,TP311.52
  13. 基于MDA的移动应用开发建模及实现,TN929.53
  14. MDA模式驱动的应用软件商店研究与实现,TP311.52
  15. 应用系统的形式化描述研究与实现,TP311.52
  16. 基于WS-CDL的贸易协同流程建模工具的研究与实现,TP393.09
  17. 社交性性取向量表在中国城市人群中的应用,C913
  18. 基于公钥加密体制的SIP协议安全模型研究与实现,TP311.52
  19. 面向自主飞行器的嵌入式系统仿真平台及其扩展应用,TP368.1
  20. 基于模型驱动体系结构的协同项目管理系统研究与开发,TP311.52

中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 计算机软件 > 程序设计、软件工程 > 软件工程 > 软件开发
© 2012 www.xueweilunwen.com