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

形式化与可视化相结合的嵌入式实时软件建模和验证

作　者: 罗浩
导　师: 张广泉
学　校: 苏州大学
专　业: 计算机软件与理论
关键词: 嵌入式实时软件建模 UML2.0顺序图时间自动机
分类号: TP311.52
类　型: 硕士论文
年　份: 2007年
下　载: 173次
引　用: 1次
阅　读: 论文下载

内容摘要

随着硬件设备计算能力的迅速提高以及社会需求的不断变化和增长,嵌入式系统变得越来越复杂,这对嵌入式实时软件开发的各个阶段(从系统分析、设计到实现、验证)均带来了新的困难和挑战。为了保障嵌入式实时软件的实时性、安全性和可靠性等,本文将基于UML的建模方法与形式化建模方法相结合,为嵌入式实时软件的建模和验证提供一种解决方案。UML2.0顺序图是UML的中描述能力最强的视图之一,它着重体现对象间动态的交互关系,并且还具有良好的易理解性。但是UML2.0顺序图用来对嵌入式实时软件建模和验证还存在时间描述方面不足之处。因此提出一种利用UML的扩展机制对UML2.0顺序图进行扩展的方法。扩展后的UML2.0顺序图不但能够很好的保持原来的易理解性,而且能够清晰的描述嵌入式实时软件的时间需求。根据扩展后UML2.0顺序图与时间自动机的语义,提出一种将扩展后UML 2.0顺序图转换成时间自动机的方法,从而将UML 2.0顺序图与时间自动机结合起来,利用UML2.0顺序图对嵌入式实时软件建模,转换成时间自动机后利用工具加以验证。最后通过对一个电梯管理系统建模和验证,把本文提出的结合思想运用到实例系统的验证当中。本文的研究对嵌入式实时软件建模和验证、UML2.0顺序图的应用和形式化方法在软件验证过程中的使用都有一定的推动作用。

全文目录

中文摘要  3-4
ABSTRACT  4-7
第一章绪论  7-11
  1.1 研究背景  7-8
  1.2 研究内容及意义  8-10
  1.3 本文组织结构  10-11
第二章形式化方法概述  11-20
  2.1 形式化描述  11-14
  2.2 形式化验证  14-20
第三章可视化建模语言UML 及其扩展  20-29
  3.1 UML 概述  20-25
    3.1.1 UML2.0 基本组成  21
    3.1.2 UML2.0 视图分析  21-23
    3.1.3 UML2.0 扩展机制  23-25
  3.2 UML2.0 顺序图  25
  3.3 UML2.0 顺序图的时序扩展  25-28
  3.4 本章小结  28-29
第四章实时顺序图的形式语义  29-38
  4.1 时间自动机概述  29-32
    4.1.1 时间自动机的定义  29-30
    4.1.2 时间自动机验证工具UPPAAL  30-32
  4.2 UML2.0 顺序图到时间自动机的转换方法  32-35
    4.2.1 简单子片段  32-33
    4.2.2 组合片段  33-35
    4.2.3 复合子片段  35
  4.3 时间自动机的优化  35-37
  4.4 本章小结  37-38
第五章实例研究  38-55
  5.1 电梯控制系统说明  38
  5.2 电梯控制系统的用例分析  38-39
  5.3 电梯控制系统的UML2.0 顺序图建模  39-48
  5.4 建立时间自动机模型  48-53
  5.5 需求验证  53-54
  5.6 本章小节  54-55
第六章总结与展望  55-57
  6.1 本文工作总结  55
  6.2 下一步工作  55-57
参考文献  57-61
攻读硕士期间参加的科研项目及发表（录用）的论文  61-62
致谢  62-63
详细摘要  63-66

形式化与可视化相结合的嵌入式实时软件建模和验证

内容摘要

全文目录

相似论文